diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-20 14:27:27 +0100 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-02-20 14:38:19 +0100 |
| commit | 8ba0292cd9299e415bc9c2c2a3307d61177f0cf5 (patch) | |
| tree | 5eade2f5d05269e767eecf8d9a1fd601c502d7c4 /reproduce/config | |
| parent | f21104afffe7a5cb28f7824211f90dc778d45b57 (diff) | |
Necessary programs checked at configure time
The mandatory and optional (for example downloader) dependencies are now
checked at configure time so users can know what they may be missing before
the processing starts. Since its recommended to be run in parallel, it can
be hard to find what you are missing after running the pipeline. As part of
these checks, the program to use for downloading is now also set at
configure time, it is only used as a pre-defined (in `LOCAL.mk') variable
during Make's processing.
A small title was also added to discus the pipeline architecture that will
be filled in the next commit.
Diffstat (limited to 'reproduce/config')
| -rw-r--r-- | reproduce/config/pipeline/LOCAL.mk.in | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/reproduce/config/pipeline/LOCAL.mk.in b/reproduce/config/pipeline/LOCAL.mk.in index ac8e10e..7a29344 100644 --- a/reproduce/config/pipeline/LOCAL.mk.in +++ b/reproduce/config/pipeline/LOCAL.mk.in @@ -68,3 +68,17 @@ BDIR = reproduce/BDIR # be defined here. This value will be used in the programs that support # this feature. MINMAPSIZE = 1000000000 + + + + + +# Downloader program +# ------------------ +# +# The downloder program (and its output option name) that will be used if +# any of the necessary datasets aren't already available on the +# system. This is usually set at an early stage of the configuration system +# automatically before the file is opened for editing by the user. It is +# thus recommended to not modify it manually. +DOWNLOADER = @downloader@ |