aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2019-02-01 12:10:44 +0000
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2019-02-01 12:10:44 +0000
commitd65b1ccd97fab64062804ace0e0ec5914e1029c1 (patch)
tree22eb65ef19b2dd6e3663789589813740b758486c
parentb9fc1c35dd8344aa78e29c6cc68acc6203ef66f8 (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.
-rw-r--r--.file-metadatabin3714 -> 3714 bytes
-rwxr-xr-xconfigure7
2 files changed, 6 insertions, 1 deletions
diff --git a/.file-metadata b/.file-metadata
index 9e9f414..579bf99 100644
--- a/.file-metadata
+++ b/.file-metadata
Binary files differ
diff --git a/configure b/configure
index 9975cae..9188f36 100755
--- a/configure
+++ b/configure
@@ -783,6 +783,11 @@ ln -s $(pwd)/reproduce/src/make/top.mk Makefile
#
# The configuration is now complete, we can inform the user on the next
# step(s) to take.
+if [ x$reproducible_paper_for_group = xyes ]; then
+ buildcommand="./for-group make -j8"
+else
+ buildcommand=".local/bin/make -j8"
+fi
cat <<EOF
----------------
@@ -791,7 +796,7 @@ The reproduction pipeline and its environment are configured with no errors.
Please run the following command to start.
(Replace '8' with the number of CPU threads)
- .local/bin/make -j8
+ $buildcommand
To change the configuration later, please re-run './configure',
DO NOT manually edit the relevant files.