mkdir -p $ISABELLE_BROWSER_INFO;
authorwenzelm
Mon, 14 Feb 2000 12:23:08 +0100
changeset 8241 a55484a9b19f
parent 8240 87e08624e209
child 8242 ac8ac0eba738
mkdir -p $ISABELLE_BROWSER_INFO;
lib/Tools/usedir
--- 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