# HG changeset patch
# User kleing
# Date 948120572 -3600
# Node ID f0d47b685433832255417a5275f75deb3a01d8b0
# Parent  b077b79061b684bd3675a88263526ad3331ff348
makes Isabelle main web pages

diff -r b077b79061b6 -r f0d47b685433 Admin/makepage
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/makepage	Mon Jan 17 15:49:32 2000 +0100
@@ -0,0 +1,70 @@
+#!/bin/bash
+#
+# $Id$
+#
+# makemainpage -- make main Isabelle web pages
+
+TARGET=/usr/proj/isabelle-repository/web
+FILES="index.html docs.html about.html cambridge.gif munich.gif"
+PREFIX=main
+
+PRG=$(basename $0)
+THIS=$(cd $(dirname "$0"); echo $PWD)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG VERSION DIST"
+  echo
+  cat <<EOF
+  Make Isabelle main web pages with links to documentation for VERSION
+
+  VERSION should be the Isabelle version contained in DIST
+  DIST should be an Isabelle distribution archive or directory
+
+EOF
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+[ $# -ne 2 ] && usage
+
+export DISTNAME=$1
+shift
+DIST=$1
+
+cd $THIS/page
+
+if [ -d $DIST ]; then
+    cp $DIST/doc/Contents .
+else
+  if [ -f $DIST ]; then
+      gzip -dc $DIST | tar -Bxf - $DISTNAME/doc/Contents 
+      mv $DISTNAME/doc/Contents .
+      rmdir -p $DISTNAME/doc
+  else 
+      echo error: $DIST not found
+      fail
+  fi
+fi
+
+make main
+
+mkdir -p $TARGET
+chgrp isabelle $TARGET
+chmod 775 $TARGET
+
+for FILE in $FILES; do
+    cp $PREFIX/$FILE $TARGET
+done
+
+cd $TARGET
+echo You should find the Isabelle pages in `pwd`
\ No newline at end of file