| author | wenzelm |
| Wed, 23 May 2012 11:53:17 +0200 | |
| changeset 48901 | 7d30534e545b |
| parent 36866 | 51af1657263b |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # mirrors the Isabelle website
5 HOST=$(hostname)
7 case ${HOST} in
8 sunbroy* | atbroy* | macbroy*)
9 DEST=/home/html/isabelle/html-data
10 ;;
11 *.cl.cam.ac.uk)
12 USER=paulson
13 DEST=/anfs/www/html/research/hvg/Isabelle
14 ;;
15 *)
16 echo "Unknown destination directory for ${HOST}"
17 exit 2
18 ;;
19 esac
21 exec $(dirname $0)/isasync $DEST