| author | wenzelm |
| Thu, 26 Nov 2009 15:03:31 +0100 | |
| changeset 33920 | 86cef0304298 |
| parent 31086 | 3e69a25b90a2 |
| child 36866 | 51af1657263b |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # $Id$
4 #
5 # mirrors the Isabelle website
7 HOST=$(hostname)
9 case ${HOST} in
10 sunbroy* | atbroy* | macbroy*)
11 DEST=/home/html/isabelle/html-data
12 ;;
13 *.cl.cam.ac.uk)
14 USER=paulson
15 DEST=/anfs/www/html/research/hvg/Isabelle
16 ;;
17 *)
18 echo "Unknown destination directory for ${HOST}"
19 exit 2
20 ;;
21 esac
23 exec $(dirname $0)/isasync $DEST