From 069d17f4f138fd779eff589119a7783784ababd9 Mon Sep 17 00:00:00 2001
From: Jim Fehrle <jfehrle@sbcglobal.net>
Date: Thu, 28 Jun 2018 13:04:27 -0700
Subject: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to
 coqtop.opt$(EXE). Fixes #7758.

---
 Makefile         | 2 +-
 Makefile.build   | 4 ++--
 Makefile.common  | 4 ++--
 Makefile.install | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index 4787377ea..0bfac2c38 100644
--- a/Makefile
+++ b/Makefile
@@ -211,7 +211,7 @@ archclean: clean-ide optclean voclean
 	rm -f $(ALLSTDLIB).*
 
 optclean:
-	rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBIN)
+	rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
diff --git a/Makefile.build b/Makefile.build
index ed251af77..60682c6e3 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -387,12 +387,12 @@ grammar/%.cmi: grammar/%.mli
 
 .PHONY: coqbinaries coqbyte
 
-coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
 coqbyte: $(TOPBYTE) $(CHICKENBYTE)
 
 # Special rule for coqtop, we imitate `ocamlopt` can delete the target
 # to avoid #7666
-$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST))
+$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST))
 	rm -f $@ && cp $< $@
 
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
diff --git a/Makefile.common b/Makefile.common
index 5b1def40a..1506bfcad 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -14,8 +14,8 @@
 # Executables
 ###########################################################################
 
-TOPBIN:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker))
-TOPBYTE:=$(TOPBIN:.opt$(EXE)=.byte$(EXE))
+TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker))
+TOPBYTE:=$(TOPBINOPT:.opt$(EXE)=.byte$(EXE))
 
 COQTOPEXE:=bin/coqtop$(EXE)
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
diff --git a/Makefile.install b/Makefile.install
index 010e35d42..21015d336 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -70,7 +70,7 @@ endif
 
 install-binaries: install-tools
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR)
 
 install-byte: install-coqide-byte
 	$(MKDIR) $(FULLBINDIR)
-- 
cgit v1.2.3


From 5d4616f63c66291d2e83c5d9847749fa89b33bf6 Mon Sep 17 00:00:00 2001
From: Jim Fehrle <jfehrle@sbcglobal.net>
Date: Thu, 28 Jun 2018 22:55:33 -0700
Subject: Suppress useless "true bin/*.opt.exe" messages from no-op STRIP and
 CODESIGN steps.

---
 Makefile.build   | 12 ++++++++++--
 Makefile.checker |  4 ++--
 Makefile.ide     | 10 +++++-----
 3 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 60682c6e3..0bc48dcf7 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -212,9 +212,17 @@ DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
 LINKMETADATA=$(if $(filter $(PRIVATEBINARIES),$@),,-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist")
 CODESIGN=$(if $(filter $(PRIVATEBINARIES),$@),true,codesign -s -)
+CODESIGN_HIDE=$(CODESIGN)
 else
 LINKMETADATA=
 CODESIGN=true
+CODESIGN_HIDE=$(HIDE)true
+endif
+
+ifeq ($(STRIP),true)
+STRIP_HIDE=$(HIDE)true
+else
+STRIP_HIDE=$(STRIP)
 endif
 
 # Best OCaml compiler, used in a generic way
@@ -400,8 +408,8 @@ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
-	$(STRIP) $@
-	$(CODESIGN) $@
+	$(STRIP_HIDE) $@
+	$(CODESIGN_HIDE) $@
 
 bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
diff --git a/Makefile.checker b/Makefile.checker
index 0ec565d61..6c19a1a42 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -52,8 +52,8 @@ ifeq ($(BEST),opt)
 $(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
-	$(STRIP) $@
-	$(CODESIGN) $@
+	$(STRIP_HIDE) $@
+	$(CODESIGN_HIDE) $@
 else
 $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
diff --git a/Makefile.ide b/Makefile.ide
index 6bb0f62f3..cb5596020 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -99,7 +99,7 @@ $(COQIDE): $(LINKIDEOPT)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
 	       -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
-	$(STRIP) $@
+	$(STRIP_HIDE) $@
 else
 $(COQIDE): $(COQIDEBYTE)
 	cp $< $@
@@ -149,8 +149,8 @@ $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
-	$(STRIP) $@
-	$(CODESIGN) $@
+	$(STRIP_HIDE) $@
+	$(CODESIGN_HIDE) $@
 
 $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
 	$(SHOW)'COQMKTOP -o $@'
@@ -229,7 +229,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
 	        -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^
-	$(STRIP) $@
+	$(STRIP_HIDE) $@
 
 $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(MKDIR) $@/coq/
@@ -275,7 +275,7 @@ $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)
 	$(INSTALLLIB) ide/MacOS/*.icns $@
 
 $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
-	$(CODESIGN) $@
+	$(CODESIGN_HIDE) $@
 
 ###########################################################################
 # CoqIde for Windows special targets
-- 
cgit v1.2.3