# HG changeset patch
# User wenzelm
# Date 950101409 -3600
# Node ID 55fed562d8ed91ecaaea4e402c5477d9f3d71573
# Parent  6be623684675840e475c47cf5ffa8d04492c2109
mirror main page;

diff -r 6be623684675 -r 55fed562d8ed Admin/mirror-main
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/mirror-main	Wed Feb 09 14:03:29 2000 +0100
@@ -0,0 +1,20 @@
+#!/bin/bash
+#
+# $Id$
+#
+
+case $(hostname) in
+  sunbroy30)
+    DEST=/home/html/isabelle/html-data
+    ;;
+  foobar)
+    DEST=/foo/bar
+    ;;
+  *)
+    echo "Unknown destination directory!"
+    exit 2
+    ;;
+esac
+
+rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
+  sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.