tuned;

--- 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]](

--- 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)
   }