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.

1 files changed, 6 insertions, 1 deletions

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.