+# 04-May-2005: if $1 is set, copy it into $MAKE, and then use $MAKE, if set,
+# instead of "make" so that if gmake is used, it is used consistently.
+
+if [ "$1" != "" ] ; then MAKE=$1 ; fi
+if [ "$MAKE" = "" ] ; then MAKE=make ; fi
+
+$MAKE buildconfig || exit 1