lib/Tools/usedir
changeset 25235 04cb7e02ca38
parent 25234 2e91cc4ddf29
child 25774 28fac5c2af54
--- a/lib/Tools/usedir	Tue Oct 30 10:51:35 2007 +0100
+++ b/lib/Tools/usedir	Tue Oct 30 10:51:35 2007 +0100
@@ -183,7 +183,7 @@
 
 # prepare browser info dir
 
-if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/library_index_header.html" ]; then
+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"
   cat "$ISABELLE_HOME/lib/html/library_index_header.template" \