diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-04-04 18:19:20 +0100 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-04-04 18:27:25 +0100 |
commit | e7b79c192bfac6c11c5f3c30fa28e8e0172c9a29 (patch) | |
tree | 6951bbc5d638fcb2a16b677c98bc380e110ae665 /reproduce/config/pipeline | |
parent | 118e6c6d3a950e4def65c64772b38b7952039b9c (diff) |
Better option checks and values in the configure script
Double quotes were placed around the checked values so they can have space
within them. Also, some checks were added for options that don't accept a
value.
Diffstat (limited to 'reproduce/config/pipeline')
0 files changed, 0 insertions, 0 deletions