src/Doc/ROOT
changeset 72103 7b318273a4aa
parent 72006 751f371d6883
child 72255 dc51115fa4aa
--- a/src/Doc/ROOT	Thu Aug 06 17:51:37 2020 +0200
+++ b/src/Doc/ROOT	Thu Aug 06 22:43:40 2020 +0200
@@ -378,7 +378,7 @@
     "root.tex"
 
 session System (doc) in "System" = Pure +
-  options [document_variants = "system", thy_output_source, pide_session]
+  options [document_variants = "system", thy_output_source]
   sessions
     "HOL-Library"
   theories