Admin/mirror-website
changeset 25463 8b9c4582795a
parent 18173 8ae6a9e7ff0e
child 27594 86db6468145d
--- a/Admin/mirror-website	Fri Nov 23 21:09:35 2007 +0100
+++ b/Admin/mirror-website	Mon Nov 26 10:42:39 2007 +0100
@@ -10,7 +10,7 @@
   sunbroy2)
     DEST=/home/html/isabelle/html-data
     ;;
-  atbroy1)
+  atbroy*)
     DEST=/home/html/isabelle/html-data
     ;;
   *.cl.cam.ac.uk)
@@ -23,4 +23,4 @@
     ;;
 esac
 
-exec $(dirname $0)/isasync -w $DEST
+exec $(dirname $0)/isasync $DEST