1.1 --- a/Admin/rsync-isabelle	Tue Mar 21 00:18:54 2000 +0100
     1.2 +++ b/Admin/rsync-isabelle	Tue Mar 21 15:23:33 2000 +0100
     1.3 @@ -12,9 +12,10 @@
     1.4  usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG [OPTIONS] [DEST]"
     1.8 +  echo "Usage: $PRG [OPTIONS] DEST"
     1.9    echo
    1.10    echo "  Options are:"
    1.11 +  echo "    -h    print help message"
    1.12    echo "    -n    dry run, don't do anything, just report what would happen"
    1.13    echo "    -d    delete files that are not on the server (beware!)"
    1.14    echo
    1.15 @@ -32,11 +33,15 @@
    1.16  
    1.17  # options
    1.18  
    1.19 +HELP=""
    1.20  ARGS=""
    1.21  
    1.22 -while getopts "nd" OPT
    1.23 +while getopts "hnd" OPT
    1.24  do
    1.25    case "$OPT" in
    1.26 +    h)
    1.27 +      HELP=true
    1.28 +      ;;
    1.29      n)
    1.30        ARGS="$ARGS -n"
    1.31        ;;
    1.32 @@ -52,6 +57,60 @@
    1.33  shift `expr $OPTIND - 1`
    1.34  
    1.35  
    1.36 +# help
    1.37 +
    1.38 +if [ -n "$HELP" ]; then
    1.39 +  cat <<EOF
    1.40 +
    1.41 +Mirroring the Isabelle Distribution
    1.42 +===================================
    1.43 +
    1.44 +The Munich site maintains an rsync server for the Isabelle
    1.45 +distribution, including complete sources, binaries, and documentation.
    1.46 +
    1.47 +The rsync tool is very smart and efficient in mirroring large
    1.48 +directory hierarchies.  See http://rsync.samba.org/ for more
    1.49 +information.  The rsync-isabelle script provides a simple front-end
    1.50 +for easy access to the Isabelle distribution.
    1.51 +
    1.52 +The script can be either run in conservative or clean-sweep mode.
    1.53 +
    1.54 +1) Basic mirroring works like this:
    1.55 +
    1.56 +  ./rsync-isabelle /foo/bar
    1.57 +
    1.58 +where /foo/bar refers to your local copy of the Isabelle distribution
    1.59 +(the base directory has to exist already).  This operation is
    1.60 +conservative in the sense that files are never deleted, thus garbage
    1.61 +may accumulate over time as our master copy is changed.
    1.62 +
    1.63 +Avoiding garbage in your local copy requires some care.  Rsync
    1.64 +provides a way to delete all additional local files that are absent in
    1.65 +the master copy.  This provides an efficient way to purge large
    1.66 +directory hierarchies, even unwillingly in case that a wrong
    1.67 +destination is given!
    1.68 +
    1.69 +2a) This will invoke a safe dry-run of clean-sweep mirroring:
    1.70 +
    1.71 +  ./rsync-isabelle -dn /foo/bar
    1.72 +
    1.73 +where additions and deletions will be printed without any actual
    1.74 +changes performed so far.
    1.75 +
    1.76 +2b) Exact mirroring with actual deletion of garbage may be performed
    1.77 +like this:
    1.78 +
    1.79 +  ./rsync-isabelle -d /foo/bar
    1.80 +
    1.81 +
    1.82 +After gaining some confidence in the workings of rsync-isabelle one
    1.83 +would usually set up some automatic mirror scheme, e.g. a daily cron
    1.84 +job run by the 'nobody' user.
    1.85 +
    1.86 +EOF
    1.87 +  exit 0
    1.88 +fi
    1.89 +
    1.90  # arguments
    1.91  
    1.92  [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }