From d65b1ccd97fab64062804ace0e0ec5914e1029c1 Mon Sep 17 00:00:00 2001
From: Mohammad Akhlaghi <mohammad@akhlaghi.org>
Date: Fri, 1 Feb 2019 12:10:44 +0000
Subject: 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.
---
 .file-metadata | Bin 3714 -> 3714 bytes
 configure      |   7 ++++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/.file-metadata b/.file-metadata
index 9e9f414..579bf99 100644
Binary files a/.file-metadata and b/.file-metadata 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.
-- 
cgit v1.2.1