Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
#!/bin/sh
#
# mirror script for isabelle distribution
#
# $Id$
#
## diagnostics
PRG=`basename "$0"`
usage()
{
echo
echo "Usage: $PRG [OPTIONS] [DEST]"
echo
echo " Options are:"
echo " -n dry run, don't do anything, just report what would happen"
echo " -d delete files that are not on the server (beware!)"
echo
exit 1
}
fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
ARGS=""
while getopts "nd" OPT
do
case "$OPT" in
n)
ARGS="$ARGS -n"
;;
d)
ARGS="$ARGS --delete"
;;
\?)
usage
;;
esac
done
shift `expr $OPTIND - 1`
# arguments
[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
DEST="$1"; shift;
## main
exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."