--- 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