author | wenzelm |
Fri, 30 Jun 2000 12:30:58 +0200 | |
changeset 9208 | 7bf28980c521 |
parent 9207 | 0c294bd701ea |
child 9209 | 862c8b83ab55 |
lib/Tools/browser | file | annotate | diff | comparison | revisions |
--- 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"