# HG changeset patch
# User wenzelm
# Date 1735222699 -3600
# Node ID 7593c0976dc6865968e6f2a44e73b2612249ebf5
# Parent 775514416939ff69871641f5b06ccb555dbbcffc
drop redundant space in HTML (see also 18a720984855);
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.output(name) + ": " + HTML.output(title) + ""
+ "" + HTML.output(name) + ": " + HTML.output(title) + ""
}
else name
}