diff -r 9146551357f6 -r 2e91cc4ddf29 lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Oct 30 10:41:19 2007 +0100
+++ b/lib/Tools/usedir	Tue Oct 30 10:51:35 2007 +0100
@@ -183,10 +183,12 @@
 
 # prepare browser info dir
 
-if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
+if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/library_index_header.html" ]; then
   mkdir -p "$ISABELLE_BROWSER_INFO"
   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
-  cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
+  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
+    "$ISABELLE_HOME/lib/html/library_index_content.template" \
+    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
 fi