changeset 9208 | 7bf28980c521 |
parent 7766 | 444ac56ead91 |
child 9237 | 161fb7f00414 |
9207:0c294bd701ea | 9208:7bf28980c521 |
---|---|
47 |
47 |
48 |
48 |
49 ## main |
49 ## main |
50 |
50 |
51 export CLASSPATH=$ISABELLE_HOME/lib/browser |
51 export CLASSPATH=$ISABELLE_HOME/lib/browser |
52 [ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO/graph/data |
52 [ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO |
53 |
53 |
54 java GraphBrowser.GraphBrowser $GRAPHFILE |
54 java GraphBrowser.GraphBrowser $GRAPHFILE |
55 [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE" |
55 [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE" |