diff options
| author | Enrico Tassi | 2015-01-16 21:09:30 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:43 +0530 |
| commit | a83721ac508aa96496ef95c8433bc282bca0db14 (patch) | |
| tree | a29ed0721b0745c06c8e74353f32c9e6c508791c /kernel/nativecode.ml | |
| 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
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions