aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-07-05 15:58:20 +0200
committerGuillaume Melquiond2016-07-05 15:58:20 +0200
commit37293bd104434bb15acc7d46b8cba90e70504aac (patch)
tree4ad0ce25dee03b9c164847cad7a0632c3c9bdb32 /kernel
parent618dce7fbf7c5b3ed80dacd16be761c4f7487079 (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')
0 files changed, 0 insertions, 0 deletions