diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-04-07 23:50:32 +0100 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-04-07 23:50:32 +0100 |
commit | 95244a0891bf9068d0e2fb22f42db234c46d8179 (patch) | |
tree | 40e8bf610c62292a7e20c6baed01b1c7ae80672f /reproduce/src | |
parent | a44c029775f512d8b92cabed7585b74d002435be (diff) |
Configure script using our build programs in final steps
In order to get a consistent final result, in its later steps, the
configure script uses our own build of the basic command-line tools (like
`cat', `awk').
Also, a correction was made to the short option parsing errors when an
unwanted argument is given, and the `-?*' was changed to `-'?'*' to avoid
un-necessary shell interpretation (for example giving unreasonable
results).
Diffstat (limited to 'reproduce/src')
0 files changed, 0 insertions, 0 deletions