# HG changeset patch
# User wenzelm
# Date 1530032593 -7200
# Node ID 16ae55c77bcb1ad372daa61d89c7e09ed760ac34
# Parent  c6626358bf21ecdc19353a59bd74d7b480deae42
clarified syntax;

diff -r c6626358bf21 -r 16ae55c77bcb src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jun 26 18:44:51 2018 +0200
+++ b/src/HOL/ROOT	Tue Jun 26 19:03:13 2018 +0200
@@ -58,7 +58,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "*=unimportant",
+  options [document_tags = "%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"
diff -r c6626358bf21 -r 16ae55c77bcb src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 18:44:51 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 19:03:13 2018 +0200
@@ -240,8 +240,8 @@
 fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
 
 fun read_tag s =
-  (case space_explode "=" s of
-    ["*", b] => (SOME b, NONE)
+  (case space_explode "%" s of
+    ["", b] => (SOME b, NONE)
   | [a, b] => (NONE, SOME (a, b))
   | _ => error ("Bad document_tags specification: " ^ quote s));