Admin/mirror-website
author haftmann
Tue, 25 Jul 2006 16:43:32 +0200
changeset 20189 1be8b181dafa
parent 18173 8ae6a9e7ff0e
child 25463 8b9c4582795a
permissions -rwxr-xr-x
added code generator serialization for Char
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17671
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     1
#!/usr/bin/env bash
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     2
#
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     3
# $Id$
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     4
#
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     5
# mirrors the Isabelle website
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     6
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     7
HOST=$(hostname)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     8
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     9
case ${HOST} in
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    10
  sunbroy2)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    11
    DEST=/home/html/isabelle/html-data
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    12
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    13
  atbroy1)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    14
    DEST=/home/html/isabelle/html-data
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    15
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    16
  *.cl.cam.ac.uk)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    17
    USER=paulson
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    18
    DEST=/anfs/www/html/Research/HVG/Isabelle
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    19
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    20
  *)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    21
    echo "Unknown destination directory for ${HOST}"
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    22
    exit 2
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    23
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    24
esac
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    25
18173
8ae6a9e7ff0e better no -d option;
wenzelm
parents: 17671
diff changeset
    26
exec $(dirname $0)/isasync -w $DEST