Admin/mirror-website
author wenzelm
Fri Feb 03 23:12:28 2006 +0100 (2006-02-03 ago)
changeset 18921 f47c46d7d654
parent 18173 8ae6a9e7ff0e
child 25463 8b9c4582795a
permissions -rwxr-xr-x
canonical member/insert/merge;
     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   atbroy1)
    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 -w $DEST