| author | bulwahn | 
| Mon, 19 Sep 2011 16:18:18 +0200 | |
| changeset 44996 | 410eea28b0f7 | 
| parent 36859 | 51af1657263b | 
| permissions | -rwxr-xr-x | 
| 17671 | 1  | 
#!/usr/bin/env bash  | 
2  | 
#  | 
|
3  | 
# mirrors the Isabelle website  | 
|
4  | 
||
5  | 
HOST=$(hostname)  | 
|
6  | 
||
7  | 
case ${HOST} in
 | 
|
| 27594 | 8  | 
sunbroy* | atbroy* | macbroy*)  | 
| 17671 | 9  | 
DEST=/home/html/isabelle/html-data  | 
10  | 
;;  | 
|
11  | 
*.cl.cam.ac.uk)  | 
|
12  | 
USER=paulson  | 
|
| 
31086
 
3e69a25b90a2
Change to lowercase path names as directed by local pagemasters
 
paulson 
parents: 
27594 
diff
changeset
 | 
13  | 
DEST=/anfs/www/html/research/hvg/Isabelle  | 
| 17671 | 14  | 
;;  | 
15  | 
*)  | 
|
16  | 
    echo "Unknown destination directory for ${HOST}"
 | 
|
17  | 
exit 2  | 
|
18  | 
;;  | 
|
19  | 
esac  | 
|
20  | 
||
| 25463 | 21  | 
exec $(dirname $0)/isasync $DEST  |