| changeset 62036 | 773cb226738c |
| parent 61974 | 5b067c681989 |
| child 62043 | f57dbc3d2a26 |
--- a/src/Tools/jEdit/etc/settings Sat Jan 02 13:29:34 2016 +0100 +++ b/src/Tools/jEdit/etc/settings Sat Jan 02 15:18:38 2016 +0100 @@ -3,7 +3,7 @@ JEDIT_HOME="$COMPONENT" JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit" -JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9" +JEDIT_OPTIONS="-reuseview -nobackground -log=9" JEDIT_JAVA_OPTIONS32="-Xms128m -Xmx1024m -Xss4m -XX:MetaspaceSize=128m" JEDIT_JAVA_OPTIONS64="-Xms512m -Xmx2560m -Xss8m -XX:MetaspaceSize=256m"