diff --git a/Makefile b/Makefile index 54fc83834d7b2260d91ab5c1fe4da2f3ecc42398..bd722b66317360562a475c1d432f76fa65191551 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,5 @@ # -# $Id: Makefile,v 1.17 1999/10/06 11:16:33 mast Exp $ +# $Id: Makefile,v 1.18 1999/10/15 23:38:11 mast Exp $ # # Meta Makefile # @@ -96,6 +96,9 @@ bin/pike: force install: @$(MAKE) "METATARGET=install" +just_verify: + @$(MAKE) $(MAKE_FLAGS) "METATARGET=just_verify" + verify: @$(MAKE) $(MAKE_FLAGS) "METATARGET=verify"