author | wenzelm |
Thu, 26 Dec 2024 15:18:19 +0100 | |
changeset 81656 | 7593c0976dc6 |
parent 81655 | 775514416939 |
child 81657 | 4210fd10e776 |
--- 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 }