author | wenzelm |
Mon, 14 Feb 2000 12:23:08 +0100 | |
changeset 8241 | a55484a9b19f |
parent 8240 | 87e08624e209 |
child 8242 | ac8ac0eba738 |
lib/Tools/usedir | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/usedir Mon Feb 14 11:23:57 2000 +0100 +++ b/lib/Tools/usedir Mon Feb 14 12:23:08 2000 +0100 @@ -102,6 +102,7 @@ if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then + mkdir -p $ISABELLE_BROWSER_INFO cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html