# HG changeset patch
# User wenzelm
# Date 1671724425 -3600
# Node ID ec07b1af45c555d3063a81a39937b5a346fe6ef5
# Parent  2afca3174629d03f7e195e7afeb3f95b284836bc
tuned;

diff -r 2afca3174629 -r ec07b1af45c5 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Thu Dec 22 16:34:35 2022 +0100
+++ b/src/Pure/Admin/build_doc.scala	Thu Dec 22 16:53:45 2022 +0100
@@ -43,8 +43,7 @@
     if (!build_results.ok) error("Build failed")
 
     progress.echo("Build started for documentation " + commas_quote(documents))
-    val doc_options = options + "document=pdf"
-    val deps = Sessions.load_structure(doc_options).selection_deps(selection)
+    val deps = Sessions.load_structure(options + "document").selection_deps(selection)
 
     val errs =
       Par_List.map[(String, String), Option[String]](
diff -r 2afca3174629 -r ec07b1af45c5 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Thu Dec 22 16:34:35 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Thu Dec 22 16:53:45 2022 +0100
@@ -118,7 +118,7 @@
     progress: Progress = new Progress,
     verbose: Boolean = false
   ): Sessions.Background = {
-      Sessions.load_structure(options + "document=pdf", dirs = dirs).
+      Sessions.load_structure(options + "document", dirs = dirs).
         selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
         background(session)
   }