# HG changeset patch
# User wenzelm
# Date 1538500800 -7200
# Node ID b7274dfbf4b35d58bfc560deae8a7cd29b3f61b1
# Parent  f33352dbbf121f67cc5728cc92cb79df434f6724
explicit group "no_doc" for unfinished documentation, allows to suppress everything uniformly: -X doc -X no_doc;

diff -r f33352dbbf12 -r b7274dfbf4b3 src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Oct 02 19:10:04 2018 +0200
+++ b/src/Doc/ROOT	Tue Oct 02 19:20:00 2018 +0200
@@ -16,7 +16,7 @@
     "root.tex"
     "style.sty"
 
-session Codegen_Basics in "Codegen" = "HOL-Library" +
+session Codegen_Basics (no_doc) in "Codegen" = "HOL-Library" +
   theories
     Setup
 
@@ -116,7 +116,7 @@
     "root.tex"
     "style.sty"
 
-session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL +
+session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL +
   options [document_variants = "how_to_prove_it", show_question_marks = false]
   theories
     How_to_Prove_it
@@ -502,6 +502,6 @@
     "root.tex"
     "style.sty"
 
-session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
+session Typeclass_Hierarchy_Basics (no_doc) in "Typeclass_Hierarchy" = "HOL-Library" +
   theories
     Setup