From 4a85cdbc0796afd2e70a7daf30967dfa2fadbafd Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Wed, 6 Feb 2019 07:24:25 -0500
Subject: Update fix-bytecode-build.patch to latest version
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The fix-bytecode-build.patch in previous commits works fine for
building and testing, but installation still fails on bytecode
platforms – the system tries to install .cmx files that don’t exist.
Update fix-bytecode-build.patch to the latest version from Gaëtan
Gilbert, which corrects the installation targets.
---
 debian/patches/fix-bytecode-build.patch | 31 ++++++++++++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

(limited to 'debian')

diff --git a/debian/patches/fix-bytecode-build.patch b/debian/patches/fix-bytecode-build.patch
index e2cdaa7d..24fbe1ec 100644
--- a/debian/patches/fix-bytecode-build.patch
+++ b/debian/patches/fix-bytecode-build.patch
@@ -1,13 +1,14 @@
 From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
 Subject: Makefiles: Fixes for byte compilation
 Bug: https://github.com/coq/coq/issues/9464
-Origin: other, https://github.com/SkySkimmer/coq/commit/4308dd8cd6deff4db946faf11822c80d16ee77ea
+Origin: other, https://github.com/SkySkimmer/coq/commit/f29aa6720eba884533972530b4283bf19d8410aa
 Reviewed-by: Benjamin Barenblat <bbaren@debian.org>
 
 - default targets don't depend on ocamlopt when it's unavailable
 - coqc.byte is built by byte target and coqc by coqbinaries target
 - unit tests use best ocaml
 - poly-capture-global-univs tests ml compilation with ocamlc
+- don't try to install .cmx and native-compute .o files
 
 Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0.
 --- a/Makefile.build
@@ -89,6 +90,20 @@ Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0.
  
  install-byte: install-coqide-byte
  	$(MKDIR) $(FULLBINDIR)
+@@ -104,11 +104,11 @@
+ 	$(MKDIR) $(FULLCOQLIB)
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)           # Regular CMI files
++	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
++ifeq ($(BEST),opt)
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMX)           # To avoid warning 58 "-opaque"
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.o)   # For static linking of plugins
+-	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
+-ifeq ($(BEST),opt)
+ 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
+ endif
+ 
 --- a/test-suite/misc/poly-capture-global-univs.sh
 +++ b/test-suite/misc/poly-capture-global-univs.sh
 @@ -11,7 +11,7 @@
@@ -100,3 +115,17 @@ Benjamin Barenblat modified this patch to apply cleanly on top of 8.9.0.
  
  if make; then
      >&2 echo 'Should have failed!'
+--- a/Makefile.vofiles
++++ b/Makefile.vofiles
+@@ -31,7 +31,10 @@
+ 
+ GLOBFILES:=$(ALLVO:.vo=.glob)
+ ifdef NATIVECOMPUTE
+-NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
++NATIVEFILES := $(call vo_to_cm,$(ALLVO))
++ifeq ($(BEST),opt)
++NATIVEFILES += $(call vo_to_obj,$(ALLVO))
++endif
+ else
+ NATIVEFILES :=
+ endif
-- 
cgit v1.2.3