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