diff options
Diffstat (limited to 'src/Makefile')
| -rw-r--r-- | src/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Makefile b/src/Makefile index a0fe6cc3..758488a2 100644 --- a/src/Makefile +++ b/src/Makefile @@ -368,7 +368,8 @@ endif $(CFG_COMPILER): $(COMPILER_INPUTS) $(CFG_BOOT) $(CFG_RUNTIME) $(CFG_STDLIB) @$(call CFG_ECHO, compile: $<) - $(CFG_QUIET)OCAMLRUNPARAM="b1" $(CFG_BOOT) $(CFG_BOOT_FLAGS) -o $@ $< + $(CFG_QUIET)OCAMLRUNPARAM="b1" $(CFG_BOOT) $(CFG_BOOT_FLAGS) \ + -minimal -o $@ $< $(CFG_QUIET)chmod 0755 $@ self: $(CFG_COMPILER) |