# HG changeset patch
# User wenzelm
# Date 1606048293 -3600
# Node ID a7877e14e7f8d2c7d65bc766b2081464ca790a4c
# Parent  dcc0022f01799fab7c99905b5f857ddb30ac5e75
proper output directory (amending cc1347c8c804);

diff -r dcc0022f0179 -r a7877e14e7f8 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Sun Nov 22 13:11:40 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Sun Nov 22 13:31:33 2020 +0100
@@ -55,7 +55,7 @@
 
             using(store.open_database_context(deps.sessions_structure))(db_context =>
               Presentation.build_documents(session, deps, db_context,
-                output_pdf = Some(Path.explode("~~/src/doc"))))
+                output_pdf = Some(Path.explode("~~/doc"))))
             None
           }
           catch {