diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-07-04 02:16:16 +0100 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-07-04 02:19:37 +0100 |
| commit | 27e9ade7bceaf0c4cfbe1bad308a5172ee801bd5 (patch) | |
| tree | 3bd518bea6183abca8950ff4b7e6f3511fb05bf2 /reproduce/analysis/make/top-make.mk | |
| parent | 318b73eee70b087735717b6eed1c91c935cb5518 (diff) | |
Some command line messages of ./project didn't mention shell
Until now, the 'shell' mode of the './project' script was missing in the
top output of './project --help' and in the error message printed when no
operation was given, or when more than one operation was given.
This is now corrected.
Diffstat (limited to 'reproduce/analysis/make/top-make.mk')
0 files changed, 0 insertions, 0 deletions