| author | wenzelm | 
| Fri, 01 Dec 2000 19:44:48 +0100 | |
| changeset 10573 | 1751ab881289 | 
| parent 10531 | a9e7786db49e | 
| child 12721 | 226fc0e2e7e3 | 
| permissions | -rwxr-xr-x | 
| 8224 | 1  | 
#!/bin/bash  | 
2  | 
#  | 
|
3  | 
# $Id$  | 
|
4  | 
#  | 
|
5  | 
||
| 8322 | 6  | 
HOST=$(hostname)  | 
7  | 
||
| 10531 | 8  | 
case ${HOST} in
 | 
| 8397 | 9  | 
sunbroy*)  | 
| 8323 | 10  | 
#test  | 
11  | 
DEST=/tmp/isabelle-dist  | 
|
12  | 
mkdir -p $DEST  | 
|
13  | 
;;  | 
|
| 8322 | 14  | 
*.cl.cam.ac.uk)  | 
15  | 
DEST=/anfs/www/html/Research/HVG/Isabelle/dist  | 
|
16  | 
;;  | 
|
| 8224 | 17  | 
*)  | 
| 8322 | 18  | 
    echo "Unknown destination directory for ${HOST}"
 | 
| 8224 | 19  | 
exit 2  | 
20  | 
;;  | 
|
21  | 
esac  | 
|
22  | 
||
| 8398 | 23  | 
exec $(dirname $0)/rsync-isabelle -d $DEST  |