diff options
| author | Maxime Dénès | 2017-03-17 08:32:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-17 08:32:54 +0100 |
| commit | f2bbdd31a6aa62d8a000f5a91f666e68e7241964 (patch) | |
| tree | 1f4192575cdde8e8f09063671c1e420884fc58e7 /dev | |
| parent | dae19c34325b2b98ee0a45ac7908a0c28021ba9e (diff) | |
| parent | a84797db94e9d242ebdf9f6feb08a63d42a14bae (diff) | |
Merge PR#445: TACTIC EXTEND now takes an optional level as argument.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions