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/_CoqProject | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/coq-makefile/only/_CoqProject

(limited to 'test-suite/coq-makefile/only/_CoqProject')

diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject
new file mode 100644
index 0000000000..357384fddf
--- /dev/null
+++ b/test-suite/coq-makefile/only/_CoqProject
@@ -0,0 +1,11 @@
+-R theories/ test
+-R src/ test
+-I src/
+
+./src/test_plugin.mlpack
+./src/test.ml4
+./src/test.mli
+./src/test_aux.ml
+./src/test_aux.mli
+./theories/test.v
+./theories/sub/testsub.v
-- 
cgit v1.2.3