drop redundant space in HTML (see also 18a720984855);
authorwenzelm
Thu, 26 Dec 2024 15:18:19 +0100
changeset 81656 7593c0976dc6
parent 81655 775514416939
child 81657 4210fd10e776
drop redundant space in HTML (see also 18a720984855);
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
   }