diff options
| author | Guillaume Melquiond | 2021-01-11 17:08:41 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-11 17:08:41 +0100 |
| commit | 94d44211fa918a75482d97cc9498811fcbcda0b2 (patch) | |
| tree | 0f2b7aa7de1c81e253c79cc3aca2025aa5d2cb95 /ide | |
| parent | 76de13a9ce03f542bca74dabee28bf27d9d8ac4f (diff) | |
Make sure Ltac2 get cleaned too.
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions