diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-08-01 12:57:10 +0100 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-08-01 12:57:10 +0100 |
| commit | baa62b742c00e47d1f44a205e935ab33e0d302aa (patch) | |
| tree | 6393c6a2350575bd517cb434a7c3a546806df421 /reproduce/analysis/config/INPUTS.mk | |
| parent | 025dee1276a39e447042cc52fd91ed001d9047d6 (diff) | |
Typo in previous commit corrected
After making the previous commit, I noticed an extra line (redundantly
defining a wrong `BASH_ENV') that should have been deleted. It has been
corrected.
Diffstat (limited to 'reproduce/analysis/config/INPUTS.mk')
0 files changed, 0 insertions, 0 deletions