# HG changeset patch
# User wenzelm
# Date 1345389694 -7200
# Node ID 20ea249bac531d74932b615bb56cd4ace590d0c9
# Parent  a7d0b9e349eca6c976833ccac9ad04993bf4873a
actually remove makeall (cf. 292b97e17fb7);

diff -r a7d0b9e349ec -r 20ea249bac53 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!"