# HG changeset patch
# User haftmann
# Date 1193737895 -3600
# Node ID 2e91cc4ddf290588d732a23aa1fa991f042d439f
# Parent  9146551357f6f21fbfab71f8a405d199c97aa01e
split library index into templates

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