| author | wenzelm |
| Fri May 11 00:43:46 2007 +0200 (2007-05-11) | |
| changeset 22932 | 53005f898665 |
| parent 18173 | 8ae6a9e7ff0e |
| child 25463 | 8b9c4582795a |
| 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 sunbroy2)
11 DEST=/home/html/isabelle/html-data
12 ;;
13 atbroy1)
14 DEST=/home/html/isabelle/html-data
15 ;;
16 *.cl.cam.ac.uk)
17 USER=paulson
18 DEST=/anfs/www/html/Research/HVG/Isabelle
19 ;;
20 *)
21 echo "Unknown destination directory for ${HOST}"
22 exit 2
23 ;;
24 esac
26 exec $(dirname $0)/isasync -w $DEST