configure: use `$make` instead of `make`

To make sure it works if `gmake` is required. Fixes: #381

configure: use `$make` instead of `make`
To make sure it works if `gmake` is required. Fixes: #381
a138b43c · Xavier Leroy · 2a9a34bc · a138b43c
Commit a138b43c authored Dec 25, 2020 by Xavier Leroy
--- 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