Admin/mirror-dist

a smaller point size reduces the number of overfull figures

#!/bin/bash
#
# $Id$
#

case $(hostname) in
  foobar)
    DEST=/foo/bar/dist
    ;;
  *)
    echo "Unknown destination directory!"
    exit 2
    ;;
esac

rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
  sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.