# HG changeset patch
# User wenzelm
# Date 886154509 -3600
# Node ID 6d0c1b2dc717dfc767f5985486160a9ba6adf395
# Parent  9e7a32dfc1f2862334c6636299c07f2511adbd72
tuned;

diff -r 9e7a32dfc1f2 -r 6d0c1b2dc717 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Jan 23 13:47:37 1998 +0100
+++ b/lib/Tools/usedir	Fri Jan 30 11:01:49 1998 +0100
@@ -78,7 +78,7 @@
 
 # prepare browser info dir
 
-if [ "$INFO" = "true" -a ! -d $ISABELLE_BROWSER_INFO ]; then
+if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
 
   mkdir -p $ISABELLE_BROWSER_INFO/gif
   cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif