lib/Tools/browser
changeset 62589 b5783412bfed
parent 61294 2d3d26e9b191
--- 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