From fd8c2ff85c098149f11280af5f1a257dd6af3622 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 1 Jun 2017 17:35:58 +0200 Subject: mention 'make world' without 'byte' in CHANGES + 2 minor suggestions --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 23c6ea6380..91b0249137 100644 --- a/Makefile +++ b/Makefile @@ -123,7 +123,7 @@ help: @echo " make clean" @echo "or make archclean" @echo "For make to be verbose, add VERBOSE=1" - @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1" + @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1" @echo @echo "Bytecode compilation is now a separate target:" @echo " make byte" -- cgit v1.2.3