# HG changeset patch
# User wenzelm
# Date 965382448 -7200
# Node ID bf459ea9a523e7156910f0c9f2ff1783447ee2f7
# Parent  c396d1092430b57b9c930ecac551c90e5a39580d
invoke isatool make in any dir containing an IsaMakefile;

diff -r c396d1092430 -r bf459ea9a523 Admin/reallymakeall
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/reallymakeall	Fri Aug 04 11:47:28 2000 +0200
@@ -0,0 +1,11 @@
+#/!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