diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-01-16 21:09:30 +0100 |
|---|---|---|
| committer |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:16:43 +0530 |
| commit | a83721ac508aa96496ef95c8433bc282bca0db14 (patch) | |
| tree | a29ed0721b0745c06c8e74353f32c9e6c508791c | |
| parent | f539df5bc1dc3541d9404238c82035ad6641dcca (diff) | |
coq_makefile: install also .v and .glob
This is useful for PIDE based interfaces, since they can
build hyperlinks out of .glob files and let the
user jump to the corresponding .v files
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index e9bdb6cac..d660f4205 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -257,7 +257,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in let cmxsfiles = List.rev_append cmofiles mllibfiles in let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] inc in let doc_dir = where_put_doc inc in let () = if is_install = Project_file.UnspecInstall then |