diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-16 11:30:16 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-16 11:30:16 +0200 |
| commit | 153651d6f959f9a18a47441f2e7280046b590f1e (patch) | |
| tree | df4a6fb46d1c7b85f0fcb48d9ce84379bf7fea91 /coq | |
| parent | 7d68132721bb4c12de8b846717972a25899ecc3f (diff) | |
| download | compcert-153651d6f959f9a18a47441f2e7280046b590f1e.tar.gz compcert-153651d6f959f9a18a47441f2e7280046b590f1e.zip | |
Added [Makefile.menhir], which gives a choice between Menhir's "code" and "table" back-ends when compiling CompCert.
For now, MENHIR_TABLE is set to false, so CompCert is not affected.
Setting MENHIR_TABLE to true builds CompCert using Menhir's table back-end.
This causes a small but repeatable slowdown on "make test", about 2% (roughly 1 second out of 40).
I have tested building ccomp and ccomp.byte.
I have tested with an ocamlfind-installed menhir and with a manually-installed menhir.
Diffstat (limited to 'coq')
0 files changed, 0 insertions, 0 deletions