diff options
| author | Gaëtan Gilbert | 2020-11-11 16:13:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-13 13:44:06 +0100 |
| commit | 76483168ec6a27a1cf456aa8ead92273e2c74bfd (patch) | |
| tree | e722a80d1429b5966b855a1b02efd7c467d3578a /engine/ftactic.ml | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
Fix incorrect "avoid" set in globenv extra data
Fix #13348
Diffstat (limited to 'engine/ftactic.ml')
0 files changed, 0 insertions, 0 deletions