From 0ca2fe2e616f303665003bc6cf2d89df385f9394 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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 --- test-suite/coq-makefile/only/run.sh | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100755 test-suite/coq-makefile/only/run.sh (limited to 'test-suite/coq-makefile/only/run.sh') diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh new file mode 100755 index 000000000..4b471bcb8 --- /dev/null +++ b/test-suite/coq-makefile/only/run.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make only TGTS="src/test.cmi src/test_aux.cmi" -j2 +test -f src/test.cmi +test -f src/test_aux.cmi +! test -f src/test.cmo -- cgit v1.2.3