author | berghofe |
Tue, 16 Oct 2001 19:56:31 +0200 | |
changeset 11813 | 5ce7346490af |
parent 11812 | 8d191eaf7fc4 |
child 11814 | 1de4a3321976 |
lib/Tools/browser | file | annotate | diff | comparison | revisions |
--- 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"