--- 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