diff -r 87e08624e209 -r a55484a9b19f 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