NEWS
changeset 68513 88b0e63d58a5
parent 68484 59793df7f853
child 68515 0854edc4d415
     1.1 --- a/NEWS	Tue Jun 26 19:03:13 2018 +0200
     1.2 +++ b/NEWS	Tue Jun 26 19:16:14 2018 +0200
     1.3 @@ -151,9 +151,9 @@
     1.4  theory Pure. Thus elementary antiquotations may be used in markup
     1.5  commands (e.g. 'chapter', 'section', 'text') and formal comments.
     1.6  
     1.7 -* System option "document_tags" specifies a default for otherwise
     1.8 -untagged commands. This is occasionally useful to control the global
     1.9 -visibility of commands via session options (e.g. in ROOT).
    1.10 +* System option "document_tags" specifies alternative command tags. This
    1.11 +is occasionally useful to control the global visibility of commands via
    1.12 +session options (e.g. in ROOT).
    1.13  
    1.14  * Document markup commands ('section', 'text' etc.) are implicitly
    1.15  tagged as "document" and visible by default. This avoids the application