diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-12 10:04:56 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-12 10:08:32 +0200 |
| commit | bd3bd1ae01bea76e0d5c4540721f7160efc3c8a8 (patch) | |
| tree | 0edb7d206e6d7d2b7d4b3e343c866b83f7bc4bf2 /Makefile.build | |
| parent | 3986eabe91a1b2b9280a711d1de86f331985c158 (diff) | |
Removing "READABLE_ML4=" from "Makefile.build"
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)) |