author | wenzelm |
Sat, 22 Aug 2009 23:24:15 +0200 | |
changeset 34665 | 27243b0128cb |
parent 34664 | 8f5fbe4a80ff |
child 34683 | fe7bedf0cfc9 |
--- a/src/Tools/jEdit/dist-template/etc/settings Sat Aug 22 23:17:09 2009 +0200 +++ b/src/Tools/jEdit/dist-template/etc/settings Sat Aug 22 23:24:15 2009 +0200 @@ -4,4 +4,4 @@ #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" JEDIT_OPTIONS="-reuseview -noserver -nobackground" -ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools" +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"