From 0ca2fe2e616f303665003bc6cf2d89df385f9394 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 23 May 2017 12:08:14 +0200
Subject: add the only target

This makes the following work correctly:
  make only TGTS="foo bar" -j2
note that
  make foo bar -j2
is not doing what you think
---
 tools/CoqMakefile.in | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tools/CoqMakefile.in')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 1de7a5c24..fdcd2ed79 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -278,6 +278,9 @@ validate: $(VOFILES)
 	$(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
 .PHONY: validate
 
+only: $(TGTS)
+.PHONY: only
+
 # Documentation targets #######################################################
 
 html: $(GLOBFILES) $(VFILES)
-- 
cgit v1.2.3