diff -r 85539b33be03 -r d0eae42f6d12 lib/Tools/usedir --- a/lib/Tools/usedir Fri May 05 22:23:27 2000 +0200 +++ b/lib/Tools/usedir Fri May 05 22:24:03 2000 +0200 @@ -106,18 +106,15 @@ # prepare browser info dir 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 + cp $ISABELLE_HOME/lib/html/index.html $ISABELLE_BROWSER_INFO/index.html mkdir -p $ISABELLE_BROWSER_INFO/graph - cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities - fi