Martine S. Lenders da3fdd33d1 tools: add capability to provide make command via environment ... Not all operating systems name the GNU Make `make`. FreeBSD e.g. uses a different dialect of Make, that seems to be incompatible with GNU make. (I wasn't able to get `make` run, but `gmake` works). This allows our test scripts to be configured via the environment variable `MAKE` to point to a different make command.		2020-07-08 09:36:36 +02:00
..
compile_test.py	tools: add capability to provide make command via environment	2020-07-08 09:36:36 +02:00