lib/Tools/browser
changeset 28500 4b79e5d3d0aa
parent 27914 9a7f17370ffb
child 28650 a7ba12e0d3b7
     1.1 --- a/lib/Tools/browser	Sat Oct 04 16:05:08 2008 +0200
     1.2 +++ b/lib/Tools/browser	Sat Oct 04 16:05:09 2008 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5  if [ -z "$GRAPHFILE" ]; then
     1.6    [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
     1.7 -  exec "$ISATOOL" java GraphBrowser.GraphBrowser
     1.8 +  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
     1.9  else
    1.10    PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
    1.11    if [ -n "$CLEAN" ]; then
    1.12 @@ -83,9 +83,9 @@
    1.13    esac
    1.14  
    1.15    if [ -z "$OUTFILE" ]; then
    1.16 -    "$ISATOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
    1.17 +    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
    1.18    else
    1.19 -    "$ISATOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
    1.20 +    "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
    1.21    fi
    1.22    RC="$?"
    1.23