changeset 11813 | 5ce7346490af |
parent 11801 | 9505bd5e9a36 |
child 11843 | 3dc60e93064f |
--- a/lib/Tools/browser Tue Oct 16 19:54:53 2001 +0200 +++ b/lib/Tools/browser Tue Oct 16 19:56:31 2001 +0200 @@ -78,7 +78,11 @@ ;; esac - java GraphBrowser.GraphBrowser "$GRAPHFILE" "$TMPOUTFILE" + if [ -z "$TMPOUTFILE" ]; then + java GraphBrowser.GraphBrowser "$GRAPHFILE" + else + java GraphBrowser.GraphBrowser "$GRAPHFILE" "$TMPOUTFILE" + fi if [ -n "$PDF" ]; then "$ISABELLE_EPSTOPDF" "$TMPOUTFILE" || fail "Failed to produce pdf output"