tuned messages;
authorwenzelm
Sun, 13 Dec 2020 13:46:28 +0100
changeset 72897 86eff7a823f3
parent 72896 4e63acc435bd
child 72898 4e4b4298f1e7
tuned messages;
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