diff -r df49b4da8903 -r 5b9bc956cec6 lib/Tools/browser --- a/lib/Tools/browser Fri Aug 15 22:58:59 2008 +0200 +++ b/lib/Tools/browser Fri Aug 15 22:59:01 2008 +0200 @@ -61,11 +61,11 @@ ## main -export CLASSPATH="$(javapath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar")" +classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" if [ -z "$GRAPHFILE" ]; then [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" - exec java GraphBrowser.GraphBrowser + javawrapper GraphBrowser.GraphBrowser else PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") if [ -n "$CLEAN" ]; then @@ -83,9 +83,9 @@ esac if [ -z "$OUTFILE" ]; then - java GraphBrowser.GraphBrowser "$(javapath "$PRIVATE_FILE")" + javawrapper GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")" else - java GraphBrowser.Console "$(javapath "$PRIVATE_FILE")" "$(javapath "$OUTFILE")" + javawrapper GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")" fi RC="$?"