#!/bin/sh
#
#	$Header: /users/jch/src/gated/src/RCS/make,v 2.0 90/04/16 16:54:38 jch Exp $
#
#	Run a make with the appropriate options.  If this fails some
#	other paths may need to be tried
#
#	If Makefile.depend does not exist, a 'make depend' is done
#	first.
#

DEPEND=Makefile.depend
CONFIG=Makefile.config
MAKEFILE=Makefile.gated

for make in /usr/bin/make /bin/make; do
	if [ -f ${make} ]; then
		if [ ! -f ${DEPEND} ]; then
			echo "Doing a make depend";
			${make} -f ${CONFIG} -f ${MAKEFILE} depend
		fi
		exec ${make} -f ${CONFIG} -f ${MAKEFILE} -f ${DEPEND} ${1+"$@"}
	fi
done

exit 1;