Tuned.
authorberghofe
Tue, 16 Oct 2001 19:56:31 +0200
changeset 11813 5ce7346490af
parent 11812 8d191eaf7fc4
child 11814 1de4a3321976
Tuned.
lib/Tools/browser
--- 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"