From d0d39968edb09c68d2143de28409d58bddcbe8cf Mon Sep 17 00:00:00 2001 From: bringert Date: Thu, 13 Dec 2007 13:28:02 +0000 Subject: [PATCH] Use $(MAKE) instead of 'make'. This should help on systems where GNU make is called gmake. --- lib/resource/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/resource/Makefile b/lib/resource/Makefile index ba8ac6bf5..d16ebef9d 100644 --- a/lib/resource/Makefile +++ b/lib/resource/Makefile @@ -23,7 +23,7 @@ GFCCP=$(GFCC) -preproc=./mkPresent .PHONY: show-path all prelude test alltenses pretest langs present mathematical multimodal compiled treebank stat gfdoc clean api new: - export GF='../../bin/gf -s' ; export GF_LIB_PATH='..'; make -e all + export GF='../../bin/gf -s' ; export GF_LIB_PATH='..'; $(MAKE) -e all all: chmod show-path prelude present alltenses mathematical api langs compiled