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.

1 files changed, 2 insertions, 2 deletions

diff --git a/configure b/configure
index 8ecb8fa..43083df 100755
--- a/configure
+++ b/configure
@@ -46,7 +46,7 @@ else
         while [ "$userread" != "y" -a "$userread" != "n" ]
         do
             echo
-            echo "------------------------------------"
+            echo "-----------------------------------------"
             echo "Reproduction pipeline local configuration"
             echo "-----------------------------------------"
             echo
@@ -55,7 +55,7 @@ else
             echo
             echo "Pressing 'y' will open the local settings file in an editor"
             echo "so you can modify the default values if you want. Each"
-            echo "variable is also thoroughly described in the comments (lines"
+            echo "variable is thoroughly described in the comments (lines"
             echo "starting with a '#') above it."
             echo
             read -p"Edit the default local configuration (y/n)? " userread