aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/coqProject_file.mli
diff options
context:
space:
mode:
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 810189450..8702da1f4 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;