diff options
| author | Guillaume Melquiond | 2016-07-05 15:58:20 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-07-05 15:58:20 +0200 |
| commit | 37293bd104434bb15acc7d46b8cba90e70504aac (patch) | |
| tree | 4ad0ce25dee03b9c164847cad7a0632c3c9bdb32 /kernel/nativecode.mli | |
| parent | 618dce7fbf7c5b3ed80dacd16be761c4f7487079 (diff) | |
Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896).
Coqc now expects physical names for input files, so fix coq_makefile
accordingly.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions