Even if we don't know what to do with the argument of the push, this at least ensures that push/pop directives stay well parenthesized.
