author | huffman |
Mon, 08 Mar 2010 14:12:51 -0800 | |
changeset 35662 | 44d7aafdddb9 |
parent 34880 | f88fc4fcab86 |
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"