diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 719046f99..f9f64071c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -66,9 +66,15 @@ DEPENDENCIES := \ # then instead of shortened version of the commands run by make # you will see the actual commands. +# If you do: +# +# READABLE_ML4=1 make +# +# then *.ml files corresponding to *.ml4 files will be generated +# in a human-readable format rather than in the binary format. + NO_RECOMPILE_ML4= NO_RECALC_DEPS= -READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library @@ -156,7 +162,11 @@ else CAMLP4USE=-D$(CAMLVERSION) endif -PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 +ifdef READABLE_ML4 +PR_O=pr_o.cmo +else +PR_O=pr_dump.cmo +endif SYSMOD:=str unix dynlink threads SYSCMA:=$(addsuffix .cma,$(SYSMOD)) |