From 9514c7dbf5a2691603a916d11ab38a34d600e501 Mon Sep 17 00:00:00 2001
From: Martin Bodin
Date: Fri, 22 May 2020 10:53:19 +0100
Subject: Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the
 parameters section.

---
 tools/CoqMakefile.in | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index a26eb9dfbe..8b0a37ee3c 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -146,6 +146,20 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
 
 TGTS ?=
 
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+# Substitution of the path by appending $(DESTDIR) if needed.
+# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
+destination_path = $(if $(DESTDIR),$(DESTDIR)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)),$(1))
+
+# Installation paths of libraries and documentation.
+COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
+COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
+COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
+
 ########## End of parameters ##################################################
 # What follows may be relevant to you only if you need to
 # extend this Makefile.  If so, look for 'Extension point' here and
@@ -227,17 +241,6 @@ else
 TIMING_ARG=
 endif
 
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
-
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -577,7 +580,7 @@ uninstall::
 	 instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
 	 rm -f "$$instf" &&\
 	 echo RM "$$instf" &&\
-	 (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+	 (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
 	done
 .PHONY: uninstall
 
-- 
cgit v1.2.3


From 4bdfeb3c6d3a90fe2980a6d9063bb00136c53eeb Mon Sep 17 00:00:00 2001
From: Martin Bodin
Date: Tue, 26 May 2020 16:44:05 +0100
Subject: Adding changelog.

---
 tools/CoqMakefile.in | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8b0a37ee3c..e2ed2db728 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -153,7 +153,8 @@ endif
 
 # Substitution of the path by appending $(DESTDIR) if needed.
 # The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
-destination_path = $(if $(DESTDIR),$(DESTDIR)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)),$(1))
+windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1))
+destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
 
 # Installation paths of libraries and documentation.
 COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
-- 
cgit v1.2.3