etc/options

--- a/etc/options	Tue Dec 05 15:19:32 2017 +0100
+++ b/etc/options	Tue Dec 05 15:29:37 2017 +0100
@@ -11,6 +11,8 @@
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
+option document_tags : string = ""
+  -- "default command tags (separated by commas)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"