| author | aspinall | 
| Fri, 30 Sep 2005 18:18:34 +0200 | |
| changeset 17740 | fc385ce6187d | 
| parent 17671 | e9e341bc7d42 | 
| child 18173 | 8ae6a9e7ff0e | 
| 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 | ||
| 26 | exec $(dirname $0)/isasync -dw $DEST |