
diff -r 775514416939 -r 7593c0976dc6 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Thu Dec 26 13:44:10 2024 +0100
+++ b/src/Pure/Tools/doc.scala	Thu Dec 26 15:18:19 2024 +0100
@@ -18,7 +18,7 @@
     def view(): Unit = Doc.view(path)
     override def toString: String =  // GUI label
       if (title.nonEmpty) {
-        "<html><b>" + HTML.output(name) + "</b>:  " + HTML.output(title) + "</html>"
+        "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
       }
       else name
   }