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 +++
 1 file changed, 3 insertions(+)
 create mode 100644 doc/changelog/08-tools/11068-coqbin-noslash.rst

(limited to 'doc')

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).
-- 
cgit v1.2.3