aboutsummaryrefslogtreecommitdiff
path: root/lib/coqProject_file.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-02-28 11:55:14 +0100
committerGaëtan Gilbert2018-02-28 12:32:59 +0100
commit195c03f798141dc816e97def7275bbdd1aa623a2 (patch)
tree5930215865bf0840ceefba46c10bdd0de87ad47b /lib/coqProject_file.mli
parente3124e098ef8170dac2b348b91757a7034bc4999 (diff)
Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSX
We fix as suggested by @JasonGross by reading file names from the _CoqProject when coq_makefile was invoked with one. I made coqdep only look at the .v files from _CoqProject because it's easier this way. Since we're going through the _CoqProject parser we could have coqdep understand more of it but let's leave that to another PR (and maybe someone else). Some projects pass vfiles on the command line, we keep the list of these files to pass them to coqdep via command line even when there is a _CoqProject. Multiple project files is probably broken.
Diffstat (limited to 'lib/coqProject_file.mli')
-rw-r--r--lib/coqProject_file.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 810189450f..8702da1f49 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -31,6 +31,7 @@ type project = {
extra_targets : extra_target list;
subdirs : string list;
+ cmdline_vfiles : string list; (** The subset of [v_files] not from the [project_file].*)
}
and extra_target = {
target : string;