-
Tamas TEVESZ authored
make is not always GNU make; the latter may go by different names. This helps builds on systems where the default make is not GNU make.
1dd18c52
make is not always GNU make; the latter may go by different names. This helps builds on systems where the default make is not GNU make.