diff -r 9fe5d8c70352 -r 0af64cc2eee9 src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Wed Nov 30 21:53:55 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Wed Nov 30 22:07:59 2022 +0100
@@ -469,9 +469,7 @@
 
     /* settings */
 
-    File.write(component_dir.settings,
-      """# -*- shell-script -*- :mode=shellscript:
-
+    component_dir.write_settings("""
 JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
 JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """
 JEDIT_JAR="$JEDIT_HOME/jedit.jar"