Admin/mirror-website
author haftmann
Wed Jan 30 10:57:47 2008 +0100 (2008-01-30)
changeset 26015 ad2756de580e
parent 25463 8b9c4582795a
child 27594 86db6468145d
permissions -rwxr-xr-x
idempotent semigroups
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # mirrors the Isabelle website
     6 
     7 HOST=$(hostname)
     8 
     9 case ${HOST} in
    10   sunbroy2)
    11     DEST=/home/html/isabelle/html-data
    12     ;;
    13   atbroy*)
    14     DEST=/home/html/isabelle/html-data
    15     ;;
    16   *.cl.cam.ac.uk)
    17     USER=paulson
    18     DEST=/anfs/www/html/Research/HVG/Isabelle
    19     ;;
    20   *)
    21     echo "Unknown destination directory for ${HOST}"
    22     exit 2
    23     ;;
    24 esac
    25 
    26 exec $(dirname $0)/isasync $DEST