diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -661,6 +661,7 @@ SHAREDIR=$sharedir COQDEVDIR=$coqdevdir OCAML_NATIVE_COMP=$ocaml_native_comp OCAML_OPT_COMP=$ocaml_opt_comp +OCAML_LM_PROF=false MENHIR_DIR=$menhir_dir COMPFLAGS=-bin-annot EOF |