From b2dd4dd979577e4f384750872f7f0e7f9bd8df94 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.ide | 45 ++++++++++++++++-----------------------------
 1 file changed, 16 insertions(+), 29 deletions(-)

(limited to 'Makefile.ide')

diff --git a/Makefile.ide b/Makefile.ide
index 0cfbdeb4e..48a269ab7 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -61,30 +61,23 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
 # CoqIde special targets
 ###########################################################################
 
-.PHONY: coqide coqide-opt coqide-byte coqide-files
-.PHONY: ide-toploop ide-byteloop ide-optloop
+.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+.PHONY: ide-toploop
 
 # target to build CoqIde
-coqide: coqide-files coqide-opt theories/Init/Prelude.vo
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
 
-ifeq ($(HASCOQIDE),opt)
-coqide-opt: $(COQIDE) ide-toploop
-else
-coqide-opt: ide-toploop
-endif
-
-ifeq ($(HASCOQIDE),no)
-coqide-byte: ide-byteloop
+coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
+coqide-no:
+coqide-byte: $(COQIDEBYTE) $(COQIDE)
+coqide-opt:  $(COQIDEBYTE) $(COQIDE)
+coqide-files: $(IDEFILES)
+ifeq ($(BEST),opt)
+ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
 else
-coqide-byte: $(COQIDEBYTE) ide-byteloop
+ide-toploop: $(IDETOPLOOPCMA)
 endif
 
-coqide-files: $(IDEFILES)
-
-ide-byteloop: $(IDETOPLOOPCMA)
-ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs)
-ide-toploop: ide-$(BEST)loop
-
 ifeq ($(HASCOQIDE),opt)
 $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
@@ -116,14 +109,14 @@ ide/%.cmo: ide/%.ml
 
 ide/%.cmx: ide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
 
 
 ####################
 ## Install targets
 ####################
 
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 
 ifeq ($(HASCOQIDE),no)
 install-coqide: install-ide-toploop
@@ -131,26 +124,20 @@ else
 install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 endif
 
-# Apparently, coqide.byte is not meant to be installed
-
-install-ide-byte:
-	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA)
-	$(MKDIR) $(FULLCOQLIB)/toploop
-	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
-
 install-ide-bin:
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
 
 install-ide-toploop:
+	$(MKDIR) $(FULLCOQLIB)/toploop
+	$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
 ifeq ($(BEST),opt)
 	$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
 endif
 
 install-ide-devfiles:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) \
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
 	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
 ifeq ($(BEST),opt)
 	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
-- 
cgit v1.2.3