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
---
 tools/CoqMakefile.in | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tools')

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