| author | wenzelm | 
| Mon, 22 Oct 2001 11:01:30 +0200 | |
| changeset 11867 | 76401b2ee871 | 
| parent 11866 | fbd097aec213 | 
| child 11868 | 56db9f3a6b3e | 
| lib/Tools/browser | file | annotate | diff | comparison | revisions | 
--- a/lib/Tools/browser Sun Oct 21 19:49:29 2001 +0200 +++ b/lib/Tools/browser Mon Oct 22 11:01:30 2001 +0200 @@ -78,7 +78,6 @@ if [ -z "$OUTFILE" ]; then java GraphBrowser.GraphBrowser "$GRAPHFILE" else - unset DISPLAY #paranoia setting java GraphBrowser.GraphBrowser "$GRAPHFILE" "$OUTFILE" fi RC="$?"