Admin/rsync-isabelle
author paulson
Mon Jul 21 13:02:07 2003 +0200 (2003-07-21)
changeset 14120 3a73850c6c7d
parent 11557 66b62cbeaab3
child 16273 3d5256d3f3f4
permissions -rwxr-xr-x
Tidied some examples
     1 #!/bin/sh
     2 #
     3 # mirror script for Isabelle distribution
     4 #
     5 # $Id$
     6 #
     7 
     8 ## diagnostics
     9 
    10 PRG=`basename "$0"`
    11 
    12 usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS] DEST"
    16   echo
    17   echo "  Options are:"
    18   echo "    -h    print help message"
    19   echo "    -n    dry run, don't do anything, just report what would happen"
    20   echo "    -d    delete files that are not on the server (BEWARE!)"
    21   echo
    22   exit 1
    23 }
    24 
    25 fail()
    26 {
    27   echo "$1" >&2
    28   exit 2
    29 }
    30 
    31 
    32 ## process command line
    33 
    34 # options
    35 
    36 HELP=""
    37 ARGS=""
    38 
    39 while getopts "hnd" OPT
    40 do
    41   case "$OPT" in
    42     h)
    43       HELP=true
    44       ;;
    45     n)
    46       ARGS="$ARGS -n"
    47       ;;
    48     d)
    49       ARGS="$ARGS --delete"
    50       ;;
    51     \?)
    52       usage
    53       ;;
    54   esac
    55 done
    56 
    57 shift `expr $OPTIND - 1`
    58 
    59 
    60 # help
    61 
    62 if [ -n "$HELP" ]; then
    63   cat <<EOF
    64 
    65 Mirroring the Isabelle Distribution
    66 ===================================
    67 
    68 The Munich site maintains an rsync server for the Isabelle
    69 distribution, including complete sources, binaries, and documentation.
    70 
    71 The rsync tool is very smart and efficient in mirroring large
    72 directory hierarchies.  See http://rsync.samba.org/ for more
    73 information.  The rsync-isabelle script provides a simple front-end
    74 for easy access to the Isabelle distribution.
    75 
    76 The script can be either run in conservative or clean-sweep mode.
    77 
    78 1) Basic mirroring works like this:
    79 
    80   ./rsync-isabelle /foo/bar
    81 
    82 where /foo/bar refers to your local copy of the Isabelle distribution
    83 (the base directory has to exist already).  This operation is
    84 conservative in the sense that files are never deleted, thus garbage
    85 may accumulate over time as our master copy is changed.
    86 
    87 Avoiding garbage in your local copy requires some care.  Rsync
    88 provides a way to delete all additional local files that are absent in
    89 the master copy.  This provides an efficient way to purge large
    90 directory hierarchies, even unwillingly in case that a wrong
    91 destination is given!
    92 
    93 2a) This will invoke a safe dry-run of clean-sweep mirroring:
    94 
    95   ./rsync-isabelle -dn /foo/bar
    96 
    97 where additions and deletions will be printed without any actual
    98 changes performed so far.
    99 
   100 2b) Exact mirroring with actual deletion of garbage may be performed
   101 like this:
   102 
   103   ./rsync-isabelle -d /foo/bar
   104 
   105 
   106 After gaining some confidence in the workings of rsync-isabelle one
   107 would usually set up some automatic mirror scheme, e.g. a daily cron
   108 job run by the 'nobody' user.
   109 
   110 EOF
   111   exit 0
   112 fi
   113 
   114 
   115 # arguments
   116 
   117 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
   118 
   119 DEST="$1"; shift;
   120 
   121 
   122 ## main
   123 
   124 exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."