diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-07 06:29:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-07 06:29:00 +0200 |
| commit | f2b28f819c16ad773ab5a2e426e3c0a478cbfdef (patch) | |
| tree | dd7e83407bc35a70b392e93d68b10df1b12343b1 /tactics | |
| parent | 82f18a32e4740c1429ac62506faff83955423417 (diff) | |
| parent | 387ed00319d7a7e8edb3644903086d2cd91eb9c7 (diff) | |
Merge PR #7706: Fix wrong deprecation msg
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions