Admin/mirror-website
changeset 17671 e9e341bc7d42
child 18173 8ae6a9e7ff0e
equal deleted inserted replaced
17670:bf4f2c1b26cc 17671:e9e341bc7d42
       
     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 -dw $DEST