diff options
Diffstat (limited to 'Makefile.config.in')
| -rw-r--r-- | Makefile.config.in | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 778c4e8..5522232 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -261,6 +261,7 @@ NOLINKALL := @NOLINKALL@ HUGE_VAL_SANITY = @HUGE_VAL_SANITY@ # Bindings that we should build -BINDINGS_TO_BUILD = @BINDINGS_TO_BUILD@ -ALL_BINDINGS = @ALL_BINDINGS@ +BINDINGS_TO_BUILD := @BINDINGS_TO_BUILD@ +ALL_BINDINGS := @ALL_BINDINGS@ +OCAML_LIBDIR := @OCAML_LIBDIR@ |