Defines the sudo set_option command. #
Allows setting undeclared options.
The command sudo set_option name val is similar to set_option name val,
but it also allows to set undeclared options.
Equations
Instances For
The command sudo set_option name val in term is similar to set_option name val in term,
but it also allows to set undeclared options.