| author | bulwahn | 
| Wed, 28 Mar 2012 10:02:22 +0200 | |
| changeset 47178 | 2ae2b6fa9c84 | 
| 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: 
27594diff
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 |