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)