diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -477,6 +477,7 @@ cat > Makefile.config <<EOF PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir +MANDIR=$sharedir/man SHAREDIR=$sharedir OCAML_OPT_COMP=$ocaml_opt_comp MENHIR_INCLUDES=$menhir_includes |