aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-03-30 10:41:32 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-03-30 11:14:19 +0200
commitc8c545713fa1e248a62fbd9905be56a5449b96a0 (patch)
tree3c265a95d5bbfd4e7fe5d1917f42d130996505ac /test-suite
parent596a4a5251cc50f50bd6d25e36c81341bf65cfed (diff)
coq_makefile: fix compilation with camlp4
Diffstat (limited to 'test-suite')
0 files changed, 0 insertions, 0 deletions