1.1 --- a/Admin/Release/mirror-website Thu Dec 05 14:35:58 2013 +0100
1.2 +++ b/Admin/Release/mirror-website Thu Dec 05 17:09:13 2013 +0000
1.3 @@ -5,12 +5,12 @@
1.4 HOST=$(hostname)
1.5
1.6 case ${HOST} in
1.7 - sunbroy* | atbroy* | macbroy* | lxbroy*)
1.8 + sunbroy* | atbroy* | macbroy*)
1.9 DEST=/home/html/isabelle/html-data
1.10 ;;
1.11 *.cl.cam.ac.uk)
1.12 USER=paulson
1.13 - DEST=/anfs/www/html/research/hvg/Isabelle
1.14 + DEST=/anfs/bigdisc/lp15/Isabelle
1.15 ;;
1.16 *)
1.17 echo "Unknown destination directory for ${HOST}"