Admin/mirror-website
author wenzelm
Thu Nov 26 15:28:42 2009 +0100 (2009-11-26)
changeset 33905 5760ba045bf0
parent 31086 3e69a25b90a2
child 36859 51af1657263b
permissions -rwxr-xr-x
additional menu entries;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # mirrors the Isabelle website
     6 
     7 HOST=$(hostname)
     8 
     9 case ${HOST} in
    10   sunbroy* | atbroy* | macbroy*)
    11     DEST=/home/html/isabelle/html-data
    12     ;;
    13   *.cl.cam.ac.uk)
    14     USER=paulson
    15     DEST=/anfs/www/html/research/hvg/Isabelle
    16     ;;
    17   *)
    18     echo "Unknown destination directory for ${HOST}"
    19     exit 2
    20     ;;
    21 esac
    22 
    23 exec $(dirname $0)/isasync $DEST