Admin/mirror-website
changeset 25463 8b9c4582795a
parent 18173 8ae6a9e7ff0e
child 27594 86db6468145d
equal deleted inserted replaced
25462:dad0291cb76a 25463:8b9c4582795a
     8 
     8 
     9 case ${HOST} in
     9 case ${HOST} in
    10   sunbroy2)
    10   sunbroy2)
    11     DEST=/home/html/isabelle/html-data
    11     DEST=/home/html/isabelle/html-data
    12     ;;
    12     ;;
    13   atbroy1)
    13   atbroy*)
    14     DEST=/home/html/isabelle/html-data
    14     DEST=/home/html/isabelle/html-data
    15     ;;
    15     ;;
    16   *.cl.cam.ac.uk)
    16   *.cl.cam.ac.uk)
    17     USER=paulson
    17     USER=paulson
    18     DEST=/anfs/www/html/Research/HVG/Isabelle
    18     DEST=/anfs/www/html/Research/HVG/Isabelle
    21     echo "Unknown destination directory for ${HOST}"
    21     echo "Unknown destination directory for ${HOST}"
    22     exit 2
    22     exit 2
    23     ;;
    23     ;;
    24 esac
    24 esac
    25 
    25 
    26 exec $(dirname $0)/isasync -w $DEST
    26 exec $(dirname $0)/isasync $DEST