author | wenzelm |
Tue, 11 May 2021 11:17:27 +0200 | |
changeset 73665 | 9ab1d5fa84d0 |
parent 73661 | 8b3e672df28c |
child 73666 | 4d0df84a5b88 |
--- a/src/Pure/Admin/build_jedit.scala Mon May 10 22:32:02 2021 +0200 +++ b/src/Pure/Admin/build_jedit.scala Tue May 11 11:17:27 2021 +0200 @@ -72,7 +72,7 @@ <!-- """ + XML.text(description) + """ mode --> <MODE> - <PROPS>""" + properties.mkString("\n", "\n", "\n") + """ + <PROPS>""" + properties.mkString("\n", "\n", "") + """ </PROPS> </MODE> """)