diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-12-01 16:36:04 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-12-01 16:38:08 +0000 |
commit | a9786200d5ed5bde30cb29b445e2a6af06694b2e (patch) | |
tree | ca1f3277f6ee724b43e458a5df25795a665827fe /reproduce/analysis/config/pdf-build.conf | |
parent | 8fbf384f7ca3d3cba566194c21da23ee6c9374be (diff) | |
parent | ac8eee90b1580fb566ee5b84fef9acb4ed437c01 (diff) |
Imported recent work in Maneage, minor conflicts fixed
Some minor conflicts that came up during the merge were fixed.
Diffstat (limited to 'reproduce/analysis/config/pdf-build.conf')
-rw-r--r-- | reproduce/analysis/config/pdf-build.conf | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/reproduce/analysis/config/pdf-build.conf b/reproduce/analysis/config/pdf-build.conf index e2d59cc..48585b4 100644 --- a/reproduce/analysis/config/pdf-build.conf +++ b/reproduce/analysis/config/pdf-build.conf @@ -3,13 +3,13 @@ # # During the project's early phases, it is usually not necessary to build # the PDF file (which makes a lot of output lines on the command-line and -# can make it hard to find the commands and possible errors (and their -# outputs). Also, in some cases, only the produced results may be of +# can make it hard to find the analysis commands and possible errors (and +# their outputs). Also, in some cases, only the produced results may be of # interest and not the final PDF, so LaTeX (and its necessary packages) may -# not be installed. +# not be installed at all. # -# If this variable is given any string, a PDF will be made with -# LaTeX. Otherwise, a notice will just printed that for now, no PDF will be +# If 'pdf-build-final' is given the value 'yes', a PDF will be made with +# LaTeX. Otherwise, a notice will just printed that, no PDF will be # created. # # Copyright (C) 2018-2020 Mohammad Akhlaghi <mohammad@akhlaghi.org> |