diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-01-16 21:09:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-01-16 21:09:30 +0100 |
| commit | 4985f0ff99278beb3b934f86edf1398659c611a8 (patch) | |
| tree | 359fd3e17cf2fb44d3d3e71379be104b4993451b /kernel/nativeinstr.mli | |
| parent | cbe7a174cf6450dcfd402d407e8afefccccde92b (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
Diffstat (limited to 'kernel/nativeinstr.mli')
0 files changed, 0 insertions, 0 deletions