# HG changeset patch
# User kleing
# Date 1032365983 -7200
# Node ID 7f5bf04095bd41796500726552c9815dc2805967
# Parent  52a419210d5c3f6d5f47995ce82591d6589081c6
comments + usage

diff -r 52a419210d5c -r 7f5bf04095bd Admin/mirror-dist
--- a/Admin/mirror-dist	Wed Sep 11 16:55:37 2002 +0200
+++ b/Admin/mirror-dist	Wed Sep 18 18:19:43 2002 +0200
@@ -2,6 +2,15 @@
 #
 # $Id$
 #
+# Mirrors the Isabelle distribution pages and downloads. 
+#
+# It does *not* mirror the home page (those directly on 
+# http://isabelle.in.tum.de). There is a separate utility 
+# (mirror-main) for that.
+#
+# Usage: mirror-dist
+#
+
 
 HOST=$(hostname)
 
diff -r 52a419210d5c -r 7f5bf04095bd Admin/mirror-main
--- a/Admin/mirror-main	Wed Sep 11 16:55:37 2002 +0200
+++ b/Admin/mirror-main	Wed Sep 18 18:19:43 2002 +0200
@@ -2,6 +2,12 @@
 #
 # $Id$
 #
+# Mirrors the Isabelle home page (those directly on http://isabelle.in.tum.de)
+# It does *not* mirror the Isabelle distribution pages and downloads. There
+# is a separate utility (mirror-dist) for that.
+#
+# Usage: mirror-main
+#
 
 HOST=$(hostname)