aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-12 16:22:20 +0200
committerMaxime Dénès2017-06-12 16:43:33 +0200
commit83d8b081c02cfde83c8fd93102f8f1aae3fe87b3 (patch)
tree53e67d72f9c7ce29e05c8c69d0e75c30c40a3cea /Makefile
parent9097e9a84cf3841cd5fac81a7fe309ae2dec246f (diff)
parentfd8c2ff85c098149f11280af5f1a257dd6af3622 (diff)
Merge PR#709: Bytecode compilation apart from 'make world', again
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile9
1 files changed, 6 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index d1fa99ccb0..91b0249137 100644
--- a/Makefile
+++ b/Makefile
@@ -116,16 +116,19 @@ NOARG: world
.PHONY: NOARG help noconfig submake
help:
- @echo "Please use either"
+ @echo "Please use either:"
@echo " ./configure"
@echo " make world"
@echo " make install"
@echo " make clean"
@echo "or make archclean"
- @echo
@echo "For make to be verbose, add VERBOSE=1"
+ @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1"
@echo
- @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1"
+ @echo "Bytecode compilation is now a separate target:"
+ @echo " make byte"
+ @echo " make install-byte"
+ @echo "Please do not mix bytecode and native targets in the same make -j"
UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
ifdef UNSAVED_FILES