src/Tools/jEdit/etc/settings
changeset 73987 fc363a3b690a
parent 71791 bb72e75cec61
child 82182 137559b26f74
--- a/src/Tools/jEdit/etc/settings	Thu Jul 15 16:01:04 2021 +0200
+++ b/src/Tools/jEdit/etc/settings	Thu Jul 15 16:35:45 2021 +0200
@@ -1,14 +1,4 @@
 # -*- shell-script -*- :mode=shellscript:
 
-JEDIT_HOME="$COMPONENT"
-JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
-
-JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
-
-JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
-JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
-
 ISABELLE_JEDIT_OPTIONS=""
-
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
-ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/dist/doc"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"