Admin/makepage
author wenzelm
Mon, 13 Mar 2000 13:21:39 +0100
changeset 8434 5e4bba59bfaa
parent 8223 960ca167cfc5
child 9287 c406d0af9368
permissions -rwxr-xr-x
use HOLogic.Not; export indexify_names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8131
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     1
#!/bin/bash
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     2
#
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     3
# $Id$
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     4
#
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     5
# makemainpage -- make main Isabelle web pages
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     6
8134
wenzelm
parents: 8131
diff changeset
     7
TARGET=/usr/proj/isabelle-repository/www
8131
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     8
FILES="index.html docs.html about.html cambridge.gif munich.gif"
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
     9
PREFIX=main
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    10
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    11
PRG=$(basename $0)
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    12
THIS=$(cd $(dirname "$0"); echo $PWD)
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    13
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    14
function usage()
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    15
{
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    16
  echo
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    17
  echo "Usage: $PRG VERSION DIST"
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    18
  echo
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    19
  cat <<EOF
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    20
  Make Isabelle main web pages with links to documentation for VERSION
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    21
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    22
  VERSION should be the Isabelle version contained in DIST
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    23
  DIST should be an Isabelle distribution archive or directory
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    24
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    25
EOF
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    26
  exit 1
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    27
}
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    28
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    29
function fail()
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    30
{
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    31
  echo "$1" >&2
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    32
  exit 2
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    33
}
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    34
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    35
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    36
## process command line
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    37
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    38
[ $# -ne 2 ] && usage
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    39
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    40
export DISTNAME=$1
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    41
shift
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    42
DIST=$1
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    43
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    44
cd $THIS/page
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    45
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    46
if [ -d $DIST ]; then
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    47
    cp $DIST/doc/Contents .
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    48
else
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    49
  if [ -f $DIST ]; then
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    50
      gzip -dc $DIST | tar -Bxf - $DISTNAME/doc/Contents 
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    51
      mv $DISTNAME/doc/Contents .
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    52
      rmdir -p $DISTNAME/doc
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    53
  else 
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    54
      echo error: $DIST not found
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    55
      fail
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    56
  fi
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    57
fi
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    58
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    59
make main
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    60
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    61
for FILE in $FILES; do
8223
wenzelm
parents: 8134
diff changeset
    62
    cp -f $PREFIX/$FILE $TARGET
8131
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    63
done
f0d47b685433 makes Isabelle main web pages
kleing
parents:
diff changeset
    64
8223
wenzelm
parents: 8134
diff changeset
    65
chmod g=u $TARGET/*
wenzelm
parents: 8134
diff changeset
    66
wenzelm
parents: 8134
diff changeset
    67
( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; )