obsolete;

--- a/Admin/reallymakeall	Sun Sep 18 15:20:08 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#/!bin/bash
-
-ISATOOL=${ISATOOL:-isatool}
-type -p "$ISATOOL" >/dev/null || { echo "isatool not found!" >&2; exit 2; }
-
-for FILE in $(find . -name IsaMakefile -print)
-do
-  DIR=$(dirname "$FILE")
-  echo "Entering $DIR ..."
-  ( cd "$DIR"; $ISATOOL make "$@"; )
-done