From ebb51092d32f8ff06423d63324e734548e1ac86e Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 19 Aug 2016 10:42:28 +0200 Subject: [PATCH] fix calling makefile on specific files --- Makefile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 6c554b275..ff1ccd39b 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ # Makefile originally taken from coq-club -%: Makefile.coq +%: Makefile.coq phony +make -f Makefile.coq $@ all: Makefile.coq @@ -17,4 +17,6 @@ _CoqProject: ; Makefile: ; -.PHONY: all clean +phony: ; + +.PHONY: all clean phony -- GitLab