changeset 53577 | d033bc00b762 |
parent 53576 | 793a429c63e7 |
child 53578 | 838d9e058a1a |
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Sep 12 13:23:54 2013 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 12 13:48:17 2013 +0200 @@ -198,8 +198,8 @@ fi fi -PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar" -GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar" +PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar" +GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/Graphview.jar" pushd "$JEDIT_HOME" >/dev/null || failed