From a138b43ccb391be63bed2fea26cd36dab96b091f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 25 Dec 2020 15:39:42 +0100
Subject: configure: use `$make` instead of `make`

To make sure it works if `gmake` is required.

Fixes: #381
---
 configure | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'configure')

diff --git a/configure b/configure
index c5afabd8..0ca893d2 100755
--- a/configure
+++ b/configure
@@ -768,7 +768,7 @@ B cparser
 B extraction
 EOF
 
-make CoqProject
+$make CoqProject
 
 #
 # Clean up target-dependent files to force their recompilation
-- 
cgit