changeset 68510 | 795f39bfe4e1 |
parent 68445 | c183a6a69f2d |
child 68512 | 16ae55c77bcb |
--- a/src/HOL/ROOT Tue Jun 26 17:25:57 2018 +0200 +++ b/src/HOL/ROOT Tue Jun 26 17:42:49 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"