| author | wenzelm | 
| Tue, 16 Sep 2008 15:37:30 +0200 | |
| changeset 28240 | 444d1e8ae496 | 
| parent 27594 | 86db6468145d | 
| child 31086 | 3e69a25b90a2 | 
| 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
 | |
| 27594 | 10 | sunbroy* | atbroy* | macbroy*) | 
| 17671 | 11 | DEST=/home/html/isabelle/html-data | 
| 12 | ;; | |
| 13 | *.cl.cam.ac.uk) | |
| 14 | USER=paulson | |
| 15 | DEST=/anfs/www/html/Research/HVG/Isabelle | |
| 16 | ;; | |
| 17 | *) | |
| 18 |     echo "Unknown destination directory for ${HOST}"
 | |
| 19 | exit 2 | |
| 20 | ;; | |
| 21 | esac | |
| 22 | ||
| 25463 | 23 | exec $(dirname $0)/isasync $DEST |