Admin/mirror-main
changeset 16292 fbe2fc30a177
parent 16278 dda44b201c4d
child 16573 cc86fd4eeee4
--- a/Admin/mirror-main	Sun Jun 05 23:07:29 2005 +0200
+++ b/Admin/mirror-main	Mon Jun 06 08:18:43 2005 +0200
@@ -12,6 +12,9 @@
 HOST=$(hostname)
 
 case ${HOST} in
+  sunbroy2)
+    DEST=/home/html/isabelle/html-data
+    ;;
   atbroy1)
     DEST=/home/html/isabelle/html-data
     ;;