tuned whitespace;
authorwenzelm
Tue, 11 May 2021 11:17:27 +0200
changeset 73921 9ab1d5fa84d0
parent 73917 8b3e672df28c
child 73922 4d0df84a5b88
tuned whitespace;
src/Pure/Admin/build_jedit.scala
--- 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>
 """)