So the question as of which directives are supported by push/pop seem to be a legitimate one. The basic rule is, as I always assumed, for every local directive as documented:QuoteThe $PUSH directive saves the current values of all local compiler directives on the settings stack
The $PUSH directive saves the current values of all local compiler directives on the settings stack
The development version of the documentation is already improved in that regard (especially note the difference between “directives” and “switches” in the first sentence).