diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-14 14:13:36 +0100 | 
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-14 14:13:36 +0100 | 
| commit | d26535d6665879f77d39e790b4aa9ee0dcb63dcf (patch) | |
| tree | abdd81f91d5fb5d11dc9e48ad39842c1cd988b62 /configure | |
| parent | 561dceda0fe880b155f8057eab78ee305ca66b80 (diff) | |
Sanity checks added, local settings now in LOCAL.mk.in
The choice of whether or not to make a PDF is now also a local system
issue, not a general pipeline issue. So it has been put in the new
`LOCAL.mk.in' file which replaces the old `DIRECTORIES.mk.in'. All local
settings (things that when changed should not be version-controlled) should
be defined in this file.
A sanity check was added to find if `./configure' has been run before
`make' or not (using the `LOCAL.mk' file which is an output of the
configuration step). If `LOCAL.mk' doesn't exist, an error will be printed
informing the user that `./configure' needs to be run first.
The configure script also provides more clear and hopefully better
information on its purpose and what must be done.
Since `make clean', it is executed even when `./configure' hasn't been run,
it will only delete the build directory and its contents when local
configuration has been done.
A `distclean' target was also added which will first "clean" the pipeline,
then delete the `LOCAL.mk.in' file.
To allow rules like `make' to be run even if `BDIR' isn't defined
(`./configure' hasn't been run yet), a fake `BDIR' is defined in such
cases.
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 57 | 
1 files changed, 31 insertions, 26 deletions
@@ -28,43 +28,37 @@  pdir=reproduce/config/pipeline -# Message to print for editing -function msg { -    echo; echo "Top-level reproduction directories are set."; -    echo "Please run the following command to start the pipeline:" -    echo "(Replace '8' with the number of CPU threads available)" -    echo; echo "    make -j8" -    echo; -} -# If `DIRECTORIES.mk' is already created, then ignore this step. -if [ -f $pdir/DIRECTORIES.mk ]; then + +# If `LOCAL.mk' is already created, then ignore this step. +if [ -f $pdir/LOCAL.mk ]; then      echo -    echo "$pdir/DIRECTORIES.mk already exists." +    echo "$pdir/LOCAL.mk already exists."      echo "To change/correct the top-level directories, please remove/edit it manually."      echo  else      # Copy the base file to the desired output file. -    if cp $pdir/DIRECTORIES.mk.in $pdir/DIRECTORIES.mk; then +    if cp $pdir/LOCAL.mk.in $pdir/LOCAL.mk; then          # Tell the user to edit the directories.          while [ "$userread" != "y" -a "$userread" != "n" ]          do -            echo "Top-level directories..."              echo -            echo "These directories define the input(s) location and the" -            echo "directory to host the intermediate/processing files." +            echo "------------------------------------" +            echo "Reproduction pipeline local configuration" +            echo "-----------------------------------------"              echo -            echo "To help in your ability to read and manage this pipeline," -            echo "it is recommended (but not mandatory) to change them to" -            echo "a directory outside this reproduction pipeline." +            echo "Local settings include things like top-level directories," +            echo "or processing steps (e.g., if you want a final PDF output)."              echo -            echo "More descriptions are provided within the file that is" -            echo "opened if you choose to edit the directories." +            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 "starting with a '#') above it."              echo -            read -p"Edit the default top-level directories (y/n)? " userread +            read -p"Edit the default local configuration (y/n)? " userread          done          # Only continue if the user wants to edit the top level @@ -72,17 +66,28 @@ else          if [ $userread = "y" ]; then              # Open a text editor to set the given directories -            if emacs $pdir/DIRECTORIES.mk;   then msg -            elif gedit $pdir/DIRECTORIES.mk; then msg -            elif vi $pdir/DIRECTORIES.mk;    then msg +            if   emacs $pdir/LOCAL.mk; then junk=1 +            elif gedit $pdir/LOCAL.mk; then junk=1 +            elif vi    $pdir/LOCAL.mk; then junk=1              else                  echo                  echo "No common text editor found on your system." -                echo "Please set the values in '$pdir/DIRECTORIES.mk' manually." +                echo "Please set the values in '$pdir/LOCAL.mk' manually."                  echo              fi          fi +        echo +        echo "This reproduction pipeline has been configured for this system." +        echo "Please run the following command to start the pipeline:" +        echo "(Replace '8' with the number of CPU threads available)" +        echo +        echo "    make -j8" +        echo +        echo +        echo "(you can always check/modify the default local settings" +        echo " by editing this file: '$pdir/LOCAL.mk')" +        echo      else -        echo; echo "Couldn't create $pdir/DIRECTORIES.mk" +        echo; echo "Couldn't create $pdir/LOCAL.mk"      fi  fi  | 
