clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: apply make utility to all logics
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [ARGS ...]"
echo
echo " Apply isabelle make to all components with IsaMakefile (passing ARGS)."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## main
[ "$1" = "-?" ] && usage
FAIL=""
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS"
for DIR in "${COMPONENTS[@]}"
do
if [ -f "$DIR/IsaMakefile" ]; then
NAME="$(basename "$DIR")"
( cd "$DIR"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$NAME "
fi
done
echo -n "Finished at "; date
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
echo "$TIMES_REPORT"
[ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"