author | wenzelm |
Fri, 30 Jan 1998 11:01:49 +0100 | |
changeset 4586 | 6d0c1b2dc717 |
parent 4585 | 9e7a32dfc1f2 |
child 4587 | 6bce9ef27d7e |
lib/Tools/usedir | file | annotate | diff | comparison | revisions |
--- 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