author | wenzelm |
Wed, 23 Dec 2009 20:35:47 +0100 | |
changeset 34804 | b0e3594c22bb |
parent 34780 | d0ff1c3a91ea |
child 34880 | f88fc4fcab86 |
permissions | -rw-r--r-- |
34664 | 1 |
JEDIT_HOME="$COMPONENT" |
2 |
||
34804
b0e3594c22bb
slightly larger stack size -- default seems to be as low as 256k;
wenzelm
parents:
34780
diff
changeset
|
3 |
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m" |
b0e3594c22bb
slightly larger stack size -- default seems to be as low as 256k;
wenzelm
parents:
34780
diff
changeset
|
4 |
#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m" |
34664 | 5 |
JEDIT_OPTIONS="-reuseview -noserver -nobackground" |
6 |
||
34780 | 7 |
ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets" |
8 |
||
34756 | 9 |
ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools" |