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