--- 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 {