diff -r 9fc75df32c81 -r ce061f5083d7 lib/Tools/browser --- a/lib/Tools/browser Sat Dec 15 20:10:26 2007 +0100 +++ b/lib/Tools/browser Sat Dec 15 21:17:48 2007 +0100 @@ -61,7 +61,8 @@ ## main -export CLASSPATH="$ISABELLE_HOME/lib/browser/GraphBrowser.jar" +export CLASSPATH="$(javapath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar")" + if [ -z "$GRAPHFILE" ]; then cd "$ISABELLE_BROWSER_INFO" exec java GraphBrowser.GraphBrowser @@ -82,9 +83,9 @@ esac if [ -z "$OUTFILE" ]; then - java GraphBrowser.GraphBrowser "$PRIVATE_FILE" + java GraphBrowser.GraphBrowser "$(javapath "$PRIVATE_FILE")" else - java GraphBrowser.Console "$PRIVATE_FILE" "$OUTFILE" + java GraphBrowser.Console "$(javapath "$PRIVATE_FILE")" "$(javapath "$OUTFILE")" fi RC="$?"