1#!/usr/bin/env bash 2# 3# mirrors the Isabelle website 4 5HOST=$(hostname) 6 7case ${HOST} in 8 sunbroy* | atbroy* | macbroy* | lxbroy*) 9 DEST=/home/html/isabelle/html-data 10 ;; 11 *.cl.cam.ac.uk) 12 USER=paulson 13 DEST=/anfs/bigdisc/lp15/Isabelle 14 ;; 15 *) 16 echo "Unknown destination directory for ${HOST}" 17 exit 2 18 ;; 19esac 20 21exec $(dirname $0)/isasync $DEST 22