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.