NEWS
changeset 68515 0854edc4d415
parent 68499 d4312962161a
parent 68513 88b0e63d58a5
child 68522 d9cbc1e8644d
--- a/NEWS	Tue Jun 26 17:22:43 2018 +0200
+++ b/NEWS	Tue Jun 26 19:29:14 2018 +0200
@@ -151,9 +151,9 @@
 theory Pure. Thus elementary antiquotations may be used in markup
 commands (e.g. 'chapter', 'section', 'text') and formal comments.
 
-* System option "document_tags" specifies a default for otherwise
-untagged commands. This is occasionally useful to control the global
-visibility of commands via session options (e.g. in ROOT).
+* System option "document_tags" specifies alternative command tags. This
+is occasionally useful to control the global visibility of commands via
+session options (e.g. in ROOT).
 
 * Document markup commands ('section', 'text' etc.) are implicitly
 tagged as "document" and visible by default. This avoids the application