changeset 9208 | 7bf28980c521 |
parent 7766 | 444ac56ead91 |
child 9237 | 161fb7f00414 |
--- a/lib/Tools/browser Fri Jun 30 10:59:50 2000 +0200 +++ b/lib/Tools/browser Fri Jun 30 12:30:58 2000 +0200 @@ -49,7 +49,7 @@ ## main export CLASSPATH=$ISABELLE_HOME/lib/browser -[ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO/graph/data +[ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO java GraphBrowser.GraphBrowser $GRAPHFILE [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE"