diff options
| author | Ralf Jung | 2017-09-20 11:51:17 +0200 |
|---|---|---|
| committer | Ralf Jung | 2017-09-20 13:53:00 +0200 |
| commit | ddf7b82220a504a8af3ac6d2dfc9664300a1db82 (patch) | |
| tree | 3f216435d63ac0797d770869c2b30a3384a6de25 /API | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
coq_makefile: dont show errors from failed (ignored) rmdir
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions