aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-12 14:46:41 +0200
committerHugo Herbelin2020-04-12 14:46:41 +0200
commit0d207dc4dc7d593c422ed81c07a7e1532899e4ec (patch)
tree9e2d656e7c66dbf9c3e377a695312d3cab28114a /Makefile.dev
parentafb4173e71f6069f7a49baf44b16569bf0cbcce4 (diff)
Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions