+# check for GNU make
+#
+MAKENAMES="gmake make no-make"
+for make in $MAKENAMES; do
+ MAKE=$make
+ $make --version 2>&1 | grep "GNU Make" >/dev/null && break
+done
+if [ $MAKE = no-make ]; then
+ echo "Fatal error: Cannot find the GNU make utility"
+ exit 1
+fi
+