Closed vpodzime closed 6 years ago
In case the 'make' executable in $PATH is not the right (GNU) 'make' to run.
Fixes #463
In case the 'make' executable in $PATH is not the right (GNU) 'make' to run.