diff -r cd266473b81b -r b5783412bfed lib/Tools/browser --- a/lib/Tools/browser Thu Mar 10 12:11:50 2016 +0100 +++ b/lib/Tools/browser Thu Mar 10 17:30:04 2016 +0100 @@ -86,9 +86,9 @@ esac if [ -z "$OUTFILE" ]; then - "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" + isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")" else - "$ISABELLE_TOOL" java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" + isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")" fi RC="$?" @@ -102,7 +102,7 @@ rm -f "$PRIVATE_FILE" elif [ -z "$ADMIN_BUILD" ]; then [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" - exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser + exec isabelle java GraphBrowser.GraphBrowser else RC=0 fi