From b2dd4dd979577e4f384750872f7f0e7f9bd8df94 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 5 Jul 2016 18:22:53 +0200
Subject: Revert "Merge remote-tracking branch 'github/pr/229' into trunk"

This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.

Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
---
 Makefile | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index db23ad0a84..93b89a4893 100644
--- a/Makefile
+++ b/Makefile
@@ -109,17 +109,14 @@ 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 "Bytecode compilation is now a separate target:"
-	@echo "   make byte"
-	@echo "   make install-byte"
-	@echo "Please do 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
-- 
cgit v1.2.3