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;
     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