# HG changeset patch
# User berghofe
# Date 1003254991 -7200
# Node ID 5ce7346490affe8b9baf152b57145d6419aff1b2
# Parent  8d191eaf7fc440771fdb49ffe43db3696ac0de80
Tuned.

diff -r 8d191eaf7fc4 -r 5ce7346490af 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"