diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/browser --- a/lib/Tools/browser Sat Oct 04 16:05:08 2008 +0200 +++ b/lib/Tools/browser Sat Oct 04 16:05:09 2008 +0200 @@ -65,7 +65,7 @@ if [ -z "$GRAPHFILE" ]; then [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" - exec "$ISATOOL" java GraphBrowser.GraphBrowser + exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser else PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") if [ -n "$CLEAN" ]; then @@ -83,9 +83,9 @@ esac if [ -z "$OUTFILE" ]; then - "$ISATOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")" + "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")" else - "$ISATOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")" + "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")" fi RC="$?"