# HG changeset patch
# User wenzelm
# Date 950103323 -3600
# Node ID 97e26127fb6b34176bcd71f3f97e9a60bc95201b
# Parent  960ca167cfc5f1594efc0e125c57357376970fc7
mirror dist page;

diff -r 960ca167cfc5 -r 97e26127fb6b Admin/mirror-dist
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/mirror-dist	Wed Feb 09 14:35:23 2000 +0100
@@ -0,0 +1,17 @@
+#!/bin/bash
+#
+# $Id$
+#
+
+case $(hostname) in
+  foobar)
+    DEST=/foo/bar/dist
+    ;;
+  *)
+    echo "Unknown destination directory!"
+    exit 2
+    ;;
+esac
+
+rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
+  sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.