On 18/09/2018 15:14, Eduardo Habkost wrote: > If it broke something, we should restore the option names and > declare them as deprecated.
I think in this particular case it's okay to add them back as no-ops, especially we'd actually want them to be customizable for user-mode emulation. Paolo
