| author | wenzelm | 
| Wed, 02 Aug 2006 22:26:46 +0200 | |
| changeset 20292 | 6f2b8ed987ec | 
| parent 18173 | 8ae6a9e7ff0e | 
| child 25463 | 8b9c4582795a | 
| permissions | -rwxr-xr-x | 
| 17671 | 1  | 
#!/usr/bin/env bash  | 
2  | 
#  | 
|
3  | 
# $Id$  | 
|
4  | 
#  | 
|
5  | 
# mirrors the Isabelle website  | 
|
6  | 
||
7  | 
HOST=$(hostname)  | 
|
8  | 
||
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  | 
|
25  | 
||
| 18173 | 26  | 
exec $(dirname $0)/isasync -w $DEST  |