diff options
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0236f19490..705d67e6c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -376,17 +376,14 @@ for records. Here are examples: Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Notations +.. flag:: Printing Notations - To deactivate the printing of all notations, use the command - ``Unset Printing Notations``. To reactivate it, use the command - ``Set Printing Notations``. - - The default is to use notations for printing terms wherever possible. + Controls whether to use notations for printing terms wherever possible. + Default is on. .. seealso:: - :opt:`Printing All` + :flag:`Printing All` To disable other elements in addition to notations. .. _locating-notations: |