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