diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-01-18 20:36:11 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-01-18 21:17:01 +0000 |
| commit | 42d3cef11bd9a84d11eb48a4ff9686d2e0ce5436 (patch) | |
| tree | 83e6252e0de115d16bcf4423ca410bd0abacd4a2 /.gitignore | |
| parent | 6a5dcc37ffd7dcc05dd786d84125366da073c43d (diff) | |
Sanity check to run the Make with proper group permissions
If the `./for-group' script is not used properly, it can lead to the whole
pipeline being re-run. Therefore it is important to do a sanity check
immediately at the start of Make's processing and inform the user if there
is a problem.
With this commit, `./for-group' exports the `reproducible_paper_for_group'
variable which is used by both the initial `./configure' script, and later
in each call to Make. The `./configure' script will use it to write a value
in `reproduce/config/pipeline/LOCAL.mk' and Make will use it to compare
with the value in `reproduce/config/pipeline/LOCAL.mk'.
If there is an inconsistency, Make will not even attempt to build anything
and will just print a message and abort.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions