aboutsummaryrefslogtreecommitdiff
path: root/reproduce/config/pipeline
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2019-02-01 18:30:02 +0000
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2019-02-01 18:38:44 +0000
commitf41be41e376dfd521881ad2e6137360e549777de (patch)
treef01dfde240cf065ea161b073ac6663a4941a2ed4 /reproduce/config/pipeline
parentd65b1ccd97fab64062804ace0e0ec5914e1029c1 (diff)
Group name is now part of the local configuration
Until now, the group name to build the project actually went into the Git source of the project! This doesn't allow exact reproducibility on different machines (where the group name may be different). With this commit, the `for-group' script has been modified to accept the group name as its first argument and pass that onto `configure' and Make. This is much better now, because not only the existance of a group installation is checked, but also the name of the group. It also made things simpler (in particular in `LOCAL.mk.in').
Diffstat (limited to 'reproduce/config/pipeline')
-rw-r--r--reproduce/config/pipeline/LOCAL.mk.in25
1 files changed, 1 insertions, 24 deletions
diff --git a/reproduce/config/pipeline/LOCAL.mk.in b/reproduce/config/pipeline/LOCAL.mk.in
index 846a5b8..41298ee 100644
--- a/reproduce/config/pipeline/LOCAL.mk.in
+++ b/reproduce/config/pipeline/LOCAL.mk.in
@@ -6,27 +6,4 @@ BDIR = @bdir@
INDIR = @indir@
DEPENDENCIES-DIR = @ddir@
DOWNLOADER = @downloader@
-FOR-GROUP = @forgroup@
-
-
-
-
-
-# In the top Makefile (which is created after running `./configure' and is
-# actually a symbolic link to `reproduce/src/make/top.mk'), we need to
-# start by checking if there is no conflict with the running and configured
-# group configuration of the pipeline.
-good-group-configuration := $(shell \
- if [ "x$(FOR-GROUP)" = xyes ]; then \
- if [ "x$(reproducible_paper_for_group)" = xyes ]; then \
- echo "yes"; \
- else \
- echo "no"; \
- fi; \
- else \
- if [ "x$(reproducible_paper_for_group)" = xyes ]; then \
- echo "no"; \
- else \
- echo "yes"; \
- fi; \
- fi)
+GROUP-NAME = @groupname@