diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-04-04 15:58:22 +0100 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-04-04 15:58:22 +0100 |
commit | 0f4a597d95f92e3a957fce7702fb39e0698ccf17 (patch) | |
tree | b8ca19b28f1240f36d53984282b0e68078a41919 /reproduce/analysis/make/top.mk | |
parent | 1418a8997ebb53ded0714673e3b334cb24a851ff (diff) |
Configure script also accepts short options with no delimiter
Until now, the short options to the configure script needed a delimiter
(either white-space or an `=') between the name and value.
With this commit, for short options, it also accepts the value immediately
touching the option name.
Also, when trying to fine the absolute address of a given path, a check was
added to abort if it doesn't exist.
Diffstat (limited to 'reproduce/analysis/make/top.mk')
0 files changed, 0 insertions, 0 deletions