diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-15 12:06:31 +0100 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-15 12:17:05 +0100 |
commit | e45ac9f074a62a0dab26e4de86e4c97458384d18 (patch) | |
tree | 40a2d6ae2c0d132a238f894f14a1df1ef517ea55 /reproduce/src | |
parent | 1d96c2922549e68922a86d307589f50a4c2b6e1b (diff) |
Choice to build final PDF removed from LOCAL settings
The previous change where we had set the building of the PDF as a local
(and thus not version controlled) setting was not good, because different
commits might be made without the high-level preparations for the final PDF
(especially during the initial/testing phases of a research). Therefore, if
the runner of the pipeline is ignorant to this, they may hit some errors in
LaTeX which can be frustrating.
To have a clean reproduction, it is thus necessary to have the choice of
pdf-building under version control along with the rest of the pipeline.
Diffstat (limited to 'reproduce/src')
0 files changed, 0 insertions, 0 deletions