# HG changeset patch # User wenzelm # Date 1216070906 -7200 # Node ID 86db6468145d079ea9d28632e9ad1e3103173378 # Parent 602dd4b219c02d8fc6a9668c3b1c7a716b91cbc1 cover macbroy as well; tuned; diff -r 602dd4b219c0 -r 86db6468145d Admin/mirror-website --- a/Admin/mirror-website Mon Jul 14 23:11:20 2008 +0200 +++ b/Admin/mirror-website Mon Jul 14 23:28:26 2008 +0200 @@ -7,10 +7,7 @@ HOST=$(hostname) case ${HOST} in - sunbroy2) - DEST=/home/html/isabelle/html-data - ;; - atbroy*) + sunbroy* | atbroy* | macbroy*) DEST=/home/html/isabelle/html-data ;; *.cl.cam.ac.uk)