diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-01-10 11:59:37 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-01-10 11:59:37 +0000 |
commit | 6dd16b871a04fe29d1805b110371b0a229876159 (patch) | |
tree | 2189887f58c94df67718c29ee09bb0a012f43c3e /reproduce/src/make/paper.mk | |
parent | dcde0ef09009a5dc1475efb1adeaebbc797cd653 (diff) |
Wrapper script to allow groups working in the build directory
On large projects, its often necessary to share the build directory between
the various users of the pipeline. To simplify the process a `for-group'
script is now added to the pipeline which is just a wrapper over the
`./configure' and `.local/bin/make' commands to make sure that the group
owner of the outputs and the permission flags are set properly.
Diffstat (limited to 'reproduce/src/make/paper.mk')
0 files changed, 0 insertions, 0 deletions