# HG changeset patch
# User wenzelm
# Date 1346172375 -7200
# Node ID f51d4a302962fe28074b60733948676b34b2abd9
# Parent  f9f900c1599e7d5d5eab9eddce0149060338154a
do not hardwire document output options -- to be provided by the user;

diff -r f9f900c1599e -r f51d4a302962 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Aug 28 17:57:47 2012 +0200
+++ b/src/HOL/ROOT	Tue Aug 28 18:46:15 2012 +0200
@@ -605,9 +605,11 @@
 session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals =
     "HOL-Ordinals_and_Cardinals-Base" +
   description {* Ordinals and Cardinals, Full Theories *}
-  options [document = pdf, document_output = "."]
   theories Cardinal_Order_Relation
-  files "document/intro.tex" "document/root.tex" "document/root.bib"
+  files
+    "document/intro.tex"
+    "document/root.tex"
+    "document/root.bib"
 
 session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" +
   description {* New (Co)datatype Package *}