I'm *for* documenting the value of push, but I think discussing it is
pointless.

However, if the value is not documented, relying on it is an error.
So either we document it, or we fix the cases where this happens in
our sources. As for what happens outside our sources, we cannot
control how people uses undocumented features.