Admin/mirror-website
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18173 8ae6a9e7ff0e
child 25463 8b9c4582795a
permissions -rwxr-xr-x
setup: theory -> theory;
haftmann@17671
     1
#!/usr/bin/env bash
haftmann@17671
     2
#
haftmann@17671
     3
# $Id$
haftmann@17671
     4
#
haftmann@17671
     5
# mirrors the Isabelle website
haftmann@17671
     6
haftmann@17671
     7
HOST=$(hostname)
haftmann@17671
     8
haftmann@17671
     9
case ${HOST} in
haftmann@17671
    10
  sunbroy2)
haftmann@17671
    11
    DEST=/home/html/isabelle/html-data
haftmann@17671
    12
    ;;
haftmann@17671
    13
  atbroy1)
haftmann@17671
    14
    DEST=/home/html/isabelle/html-data
haftmann@17671
    15
    ;;
haftmann@17671
    16
  *.cl.cam.ac.uk)
haftmann@17671
    17
    USER=paulson
haftmann@17671
    18
    DEST=/anfs/www/html/Research/HVG/Isabelle
haftmann@17671
    19
    ;;
haftmann@17671
    20
  *)
haftmann@17671
    21
    echo "Unknown destination directory for ${HOST}"
haftmann@17671
    22
    exit 2
haftmann@17671
    23
    ;;
haftmann@17671
    24
esac
haftmann@17671
    25
wenzelm@18173
    26
exec $(dirname $0)/isasync -w $DEST