changeset 13567 | 7f5bf04095bd |
parent 12721 | 226fc0e2e7e3 |
--- 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)