# HG changeset patch
# User wenzelm
# Date 1607863588 -3600
# Node ID 86eff7a823f3665bedf50ad0c400d6da0ca3929b
# Parent  4e63acc435bd47e2b0e9ee4d5737ef31441e6613
tuned messages;

diff -r 4e63acc435bd -r 86eff7a823f3 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Sun Dec 13 13:44:50 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Sun Dec 13 13:46:28 2020 +0100
@@ -51,7 +51,7 @@
       {
         case (doc, session) =>
           try {
-            progress.echo("Documentation " + doc + " ...")
+            progress.echo("Documentation " + quote(doc) + " ...")
 
             using(store.open_database_context())(db_context =>
               Presentation.build_documents(session, deps, db_context,
@@ -61,7 +61,7 @@
           catch {
             case Exn.Interrupt.ERROR(msg) =>
               val sep = if (msg.contains('\n')) "\n" else " "
-              Some("Documentation " + doc + " failed:" + sep + msg)
+              Some("Documentation " + quote(doc) + " failed:" + sep + msg)
           }
       }, selected).flatten