From 2f7cf5ae0c22bc802f75cccbd863be2c23630496 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Nov 2019 16:04:11 +0100
Subject: coq_makefile: support COQBIN with no ending /

Close #6460
---
 doc/changelog/08-tools/11068-coqbin-noslash.rst | 3 +++
 tools/CoqMakefile.in                            | 5 +++++
 2 files changed, 8 insertions(+)
 create mode 100644 doc/changelog/08-tools/11068-coqbin-noslash.rst

diff --git a/doc/changelog/08-tools/11068-coqbin-noslash.rst b/doc/changelog/08-tools/11068-coqbin-noslash.rst
new file mode 100644
index 0000000000..c2c8f4df31
--- /dev/null
+++ b/doc/changelog/08-tools/11068-coqbin-noslash.rst
@@ -0,0 +1,3 @@
+- ``coq_makefile`` now supports environment variable ``COQBIN`` with
+  no ending ``/`` character (`#11068
+  <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert).
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index abfbd66e28..27f9a0f8c6 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -78,6 +78,11 @@ else
 STDTIME?=command time -f $(TIMEFMT)
 endif
 
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+endif
+
 # Coq binaries
 COQC     ?= "$(COQBIN)coqc"
 COQTOP   ?= "$(COQBIN)coqtop"
-- 
cgit v1.2.3