diff options
| author | Maxime Dénès | 2018-09-26 15:53:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 15:53:19 +0200 |
| commit | db29b49361689d9cbc5c4dc61e829d3e40bcb425 (patch) | |
| tree | 271bbf390613e8f3157a1a861824ae5c228f67a7 /dev | |
| parent | 8c3f395e52020f82822100730026a950c3653c8c (diff) | |
| parent | 7dcc01273a18afc2921c567574c76b411c1b63d9 (diff) | |
Merge PR #8497: Use "rm -rf" in "make clean" so .coq-native directories are removed
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions