doc-src/ROOT
changeset 48943 54da920baf38
parent 48942 75d8778f94d3
child 48944 ac15a85e9282
--- a/doc-src/ROOT	Mon Aug 27 21:04:37 2012 +0200
+++ b/doc-src/ROOT	Mon Aug 27 21:19:16 2012 +0200
@@ -101,13 +101,15 @@
     "~~/src/HOL/Library/OptionalSugar"
   theories Sugar
 
-session Locales (doc) in "Locales/Locales" = HOL +
-  options [browser_info = false, document = false,
-    document_dump = document, document_dump_mode = "tex"]
+session Locales (doc) in "Locales" = HOL +
+  options [document_variants = "locales"]
   theories
     Examples1
     Examples2
     Examples3
+  files
+    "document/build"
+    "document/root.tex"
 
 session Logics (doc) in "Logics" = Pure +
   options [document_variants = "logics"]