Admin/Release/mirror-website

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