diff options
| author | Maxime Dénès | 2017-09-22 11:20:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-22 11:20:13 +0200 |
| commit | 6d3b6c3c1f798ace3b57048401069ec52532d6ed (patch) | |
| tree | 8d7a44889c35d6aee02eaafce2c0fb232e3bcbbe /API | |
| parent | 809fab2fde0c8dbd8ea940c563be9ab5f988d9d0 (diff) | |
| parent | ddf7b82220a504a8af3ac6d2dfc9664300a1db82 (diff) | |
Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions