#!/bin/bash # # $Id$ # HOST=$(hostname) case ${HOST} in sunbroy*) #test DEST=/tmp/isabelle-dist mkdir -p $DEST ;; *.cl.cam.ac.uk) DEST=/anfs/www/html/Research/HVG/Isabelle/dist ;; *) echo "Unknown destination directory for ${HOST}" exit 2 ;; esac exec $(dirname $0)/rsync-isabelle -d $DEST