src/Pure/Admin/build_release.scala
changeset 73112 efc58b56a6c7
parent 73095 d08cbc36a99a
child 73152 5a954fd5f078
--- a/src/Pure/Admin/build_release.scala	Fri Jan 08 23:59:28 2021 +0100
+++ b/src/Pure/Admin/build_release.scala	Sat Jan 09 00:11:52 2021 +0100
@@ -642,8 +642,7 @@
 
           case Platform.Family.macos =>
             File.change(isabelle_target + jedit_props,
-              _.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
-               .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+              _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
                .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
 
 
@@ -692,9 +691,7 @@
 
           case Platform.Family.windows =>
             File.change(isabelle_target + jedit_props,
-              _.replaceAll("lookAndFeel=.*",
-                  "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
-               .replaceAll("foldPainter=.*", "foldPainter=Square"))
+              _.replaceAll("foldPainter=.*", "foldPainter=Square"))
 
 
             // application launcher