NEWS
changeset 68515 0854edc4d415
parent 68495 d4312962161a
parent 68513 88b0e63d58a5
child 68522 d9cbc1e8644d
     1.1 --- a/NEWS	Tue Jun 26 17:22:43 2018 +0200
     1.2 +++ b/NEWS	Tue Jun 26 19:29: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