--- a/Admin/makepage Mon Sep 11 18:00:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-#!/bin/bash
-#
-# $Id$
-#
-# makemainpage -- make main Isabelle web pages
-
-TARGET=/usr/proj/isabelle-repository/www
-FILES="index.html docs.html logics.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
-
-for FILE in $FILES; do
- cp -f $PREFIX/$FILE $TARGET
-done
-
-chmod g=u $TARGET/*
-
-( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; )