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/config/pipeline/INPUTS.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/config/pipeline/INPUTS.mk')
0 files changed, 0 insertions, 0 deletions