--- 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)
--- 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)