diff options
| author | Gaëtan Gilbert | 2020-02-06 14:50:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 92d34ac2a926ebbe7a1cf339bd3cce0c529a99ec (patch) | |
| tree | 748193fd5f6a81cfc202318a95d438165b4f1e37 /plugins | |
| parent | 3fcf06878d10a4a0c17d7095da964ebf15ed922b (diff) | |
unsafe_type_of + match -> sort_of in Tactics.cut
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions