Admin/Release/mirror-website
author hoelzl
Tue Mar 26 12:20:55 2013 +0100 (2013-03-26)
changeset 51521 36fa825e0ea7
parent 51087 175b43e0b9ce
child 54636 cc126144f662
permissions -rwxr-xr-x
merge RComplete into RealDef
     1 #!/usr/bin/env bash
     2 #
     3 # mirrors the Isabelle website
     4 
     5 HOST=$(hostname)
     6 
     7 case ${HOST} in
     8   sunbroy* | atbroy* | macbroy* | lxbroy*)
     9     DEST=/home/html/isabelle/html-data
    10     ;;
    11   *.cl.cam.ac.uk)
    12     USER=paulson
    13     DEST=/anfs/www/html/research/hvg/Isabelle
    14     ;;
    15   *)
    16     echo "Unknown destination directory for ${HOST}"
    17     exit 2
    18     ;;
    19 esac
    20 
    21 exec $(dirname $0)/isasync $DEST