Admin/mirror-dist
changeset 13567 7f5bf04095bd
parent 12721 226fc0e2e7e3
     1.1 --- a/Admin/mirror-dist	Wed Sep 11 16:55:37 2002 +0200
     1.2 +++ b/Admin/mirror-dist	Wed Sep 18 18:19:43 2002 +0200
     1.3 @@ -2,6 +2,15 @@
     1.4  #
     1.5  # $Id$
     1.6  #
     1.7 +# Mirrors the Isabelle distribution pages and downloads. 
     1.8 +#
     1.9 +# It does *not* mirror the home page (those directly on 
    1.10 +# http://isabelle.in.tum.de). There is a separate utility 
    1.11 +# (mirror-main) for that.
    1.12 +#
    1.13 +# Usage: mirror-dist
    1.14 +#
    1.15 +
    1.16  
    1.17  HOST=$(hostname)
    1.18