actually remove makeall (cf. 292b97e17fb7);
authorwenzelm
Sun, 19 Aug 2012 17:21:34 +0200
changeset 48856 20ea249bac53
parent 48855 a7d0b9e349ec
child 48857 9032f4bdf205
actually remove makeall (cf. 292b97e17fb7);
lib/Tools/makeall
--- a/lib/Tools/makeall	Fri Aug 17 21:16:13 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-#!/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"
-
-splitarray ":" "$ISABELLE_COMPONENTS"; COMPONENTS=("${SPLITARRAY[@]}")
-
-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!"