diff options
| author | Gaëtan Gilbert | 2019-10-30 16:10:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-30 16:11:12 +0100 |
| commit | fe61f673dfdba1598842b9d56a761c5229aaf4e9 (patch) | |
| tree | 7f8944287a502bde0df44c81f188cfe4f59cd32c /dev | |
| parent | dbcdc4e53758339d2a7eb96d19fbcffeb143154d (diff) | |
make: guard cp calls with rm -f on executables
Fix #10728
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions