backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
#!/usr/bin/env bash
#
# Author: Stefan Berghofer, TU Muenchen
# Author: Makarius
#
# DESCRIPTION: display Isabelle version
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS]"
echo
echo " Options are:"
echo " -i short identification (derived from Mercurial id)"
echo
echo " Display Isabelle version information."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
SHORT_ID=""
while getopts "i" OPT
do
case "$OPT" in
i)
SHORT_ID=true
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -ne 0 ] && usage
## main
if [ -n "$SHORT_ID" ]; then
if [ -n "$ISABELLE_ID" ]; then
echo "$ISABELLE_ID"
else
"${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || echo undefined
fi
else
echo 'repository version' # filled in automatically!
fi