haftmann@17671: #!/usr/bin/env bash
haftmann@17671: #
haftmann@17671: # $Id$
haftmann@17671: #
haftmann@17671: # mirrors the Isabelle website
haftmann@17671: 
haftmann@17671: HOST=$(hostname)
haftmann@17671: 
haftmann@17671: case ${HOST} in
haftmann@17671:   sunbroy2)
haftmann@17671:     DEST=/home/html/isabelle/html-data
haftmann@17671:     ;;
haftmann@17671:   atbroy1)
haftmann@17671:     DEST=/home/html/isabelle/html-data
haftmann@17671:     ;;
haftmann@17671:   *.cl.cam.ac.uk)
haftmann@17671:     USER=paulson
haftmann@17671:     DEST=/anfs/www/html/Research/HVG/Isabelle
haftmann@17671:     ;;
haftmann@17671:   *)
haftmann@17671:     echo "Unknown destination directory for ${HOST}"
haftmann@17671:     exit 2
haftmann@17671:     ;;
haftmann@17671: esac
haftmann@17671: 
wenzelm@18173: exec $(dirname $0)/isasync -w $DEST