lib/Tools/usedir
changeset 8810 d0eae42f6d12
parent 8747 22580c8bc62f
child 9047 810966809663
--- 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