author | wenzelm |
Tue, 12 Jan 2010 16:51:51 +0100 | |
changeset 34880 | f88fc4fcab86 |
parent 34804 | b0e3594c22bb |
child 36101 | bae883012af3 |
permissions | -rw-r--r-- |
JEDIT_HOME="$COMPONENT" JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit" JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m" #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m" JEDIT_OPTIONS="-reuseview -noserver -nobackground" ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets" ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"