src/Doc/ROOT
changeset 73739 3e44f8c3f059
parent 73734 f7f0d516df0c
child 73744 beeebae99746
--- a/src/Doc/ROOT	Wed May 19 11:18:38 2021 +0200
+++ b/src/Doc/ROOT	Wed May 19 11:48:35 2021 +0200
@@ -326,13 +326,11 @@
     "root.tex"
 
 session Main (doc) in "Main" = HOL +
-  options [document_build = "build", document_variants = "main"]
+  options [document_variants = "main"]
   theories Main_Doc
   document_files (in "..")
-    "prepare_document"
     "pdfsetup.sty"
   document_files
-    "build"
     "root.tex"
 
 session Nitpick (doc) in "Nitpick" = Pure +