diff options
Diffstat (limited to 'lib/coqProject_file.mli')
-rw-r--r-- | lib/coqProject_file.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 2bcf658fc..8c8fc068a 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -21,13 +21,16 @@ type project = { mllib_files : string list; mlpack_files : string list; - extra_targets : extra_target list; - subdirs : string list; ml_includes : path list; r_includes : (path * logic_path) list; q_includes : (path * logic_path) list; extra_args : string list; defs : (string * string) list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target list; + subdirs : string list; + } and extra_target = { target : string; |