diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -151,6 +151,7 @@ driver/Configuration.ml: Makefile.config echo 'let arch = "$(ARCH)"'; \ echo 'let variant = "$(VARIANT)"'; \ echo 'let system = "$(SYSTEM)"'; \ + echo 'let signed_char = $(SIGNED_CHAR)'; \ echo 'let need_stdlib_wrapper = $(NEED_STDLIB_WRAPPER)') \ > driver/Configuration.ml |