diff options
author | Joachim Breitner <mail@joachim-breitner.de> | 2018-02-12 10:32:01 -0500 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-02-15 10:21:31 +0100 |
commit | 00dfe2be53ddc84836e095f0a20a0efdebc87f50 (patch) | |
tree | d2263783fafba64e1eab2af888342e5001f1a8c6 /test-suite/coq-makefile | |
parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) |
coq_makefile: Support "" as the prefix in _CoqProject
This fixes #6350 (and even comes with a test case).
Refering to other directories as `-R … ""` is maybe not best practice,
but some people out there do it, so as long as it does not cause too
much trouble, we can continue to support it.
Diffstat (limited to 'test-suite/coq-makefile')
-rw-r--r-- | test-suite/coq-makefile/emptyprefix/_CoqProject | 11 | ||||
-rw-r--r-- | test-suite/coq-makefile/emptyprefix/_CoqProject.sub | 3 | ||||
-rwxr-xr-x | test-suite/coq-makefile/emptyprefix/run.sh | 17 |
3 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject new file mode 100644 index 000000000..5678a8edb --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -0,0 +1,11 @@ +-R theories "" +-R src "" +-I src +-arg "-w default" + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject.sub b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub new file mode 100644 index 000000000..90ac541e0 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject.sub @@ -0,0 +1,3 @@ +-R ../theories "" +-I ../src +testsub.v diff --git a/test-suite/coq-makefile/emptyprefix/run.sh b/test-suite/coq-makefile/emptyprefix/run.sh new file mode 100755 index 000000000..a10e63b42 --- /dev/null +++ b/test-suite/coq-makefile/emptyprefix/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +set -e + +. ../template/init.sh + +mv theories/sub theories2 + +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make + +cp ../_CoqProject.sub theories2/_CoqProject +cd theories2 +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +make |