# HG changeset patch
# User wenzelm
# Date 1659626096 -7200
# Node ID 5ad049a5f6a814ecb7bc7a96e8f671f5f8b86d11
# Parent  6f5fc43a3e454ca87b697de8715242ca0c000fce
tuned;

diff -r 6f5fc43a3e45 -r 5ad049a5f6a8 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Thu Aug 04 17:08:35 2022 +0200
+++ b/src/Pure/Admin/build_doc.scala	Thu Aug 04 17:14:56 2022 +0200
@@ -54,9 +54,10 @@
             progress.expose_interrupt()
             progress.echo("Documentation " + quote(doc) + " ...")
 
-            using(store.open_database_context())(db_context =>
+            using(store.open_database_context()) { db_context =>
               Document_Build.build_documents(Document_Build.context(session, deps, db_context),
-                output_pdf = Some(Path.explode("~~/doc"))))
+                output_pdf = Some(Path.explode("~~/doc")))
+            }
             None
           }
           catch {