diff options
| author | Pierre-Marie Pédrot | 2017-04-16 20:37:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-24 17:59:21 +0200 |
| commit | 98da9fdce866728f93bc7cb690275f5559aa9bae (patch) | |
| tree | bc01065a1cca18ded5aa221e3c9e1a7c7ad316d8 /dev/header | |
| parent | a1fd5fb489237a1300adb242e2c9b6c74c82981b (diff) | |
Removing various tactic compatibility layers in core tactics.
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions