| author | wenzelm |
| Fri Feb 03 23:12:28 2006 +0100 (2006-02-03 ago) | |
| changeset 18921 | f47c46d7d654 |
| 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