diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-02-01 12:10:44 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-02-01 12:10:44 +0000 |
| commit | d65b1ccd97fab64062804ace0e0ec5914e1029c1 (patch) | |
| tree | 22eb65ef19b2dd6e3663789589813740b758486c /reproduce/analysis/make/top.mk | |
| parent | b9fc1c35dd8344aa78e29c6cc68acc6203ef66f8 (diff) | |
Configure script ending message now accounts for group building
Until now, the `./configure' script would only print the `.local/bin/make
-j8' command. But when configured for groups, a different command should be
used. It now does a check just before running and suggests the proper
command.
Diffstat (limited to 'reproduce/analysis/make/top.mk')
0 files changed, 0 insertions, 0 deletions