# HG changeset patch
# User wenzelm
# Date 1003857178 -7200
# Node ID f8f37d61fbc223175d33e4f991bb2daad38f953e
# Parent  e543b0f01a58f5ec089e4eb8fc6853860e1eef5e
unset DISPLAY (again);

diff -r e543b0f01a58 -r f8f37d61fbc2 lib/Tools/browser
--- a/lib/Tools/browser	Tue Oct 23 19:12:37 2001 +0200
+++ b/lib/Tools/browser	Tue Oct 23 19:12:58 2001 +0200
@@ -78,6 +78,7 @@
   if [ -z "$OUTFILE" ]; then
     java GraphBrowser.GraphBrowser "$GRAPHFILE"
   else
+    unset DISPLAY  #paranoia setting
     java GraphBrowser.GraphBrowser "$GRAPHFILE" "$OUTFILE"
   fi
   RC="$?"