diff options
author | 2014-10-09 15:36:13 +0200 | |
---|---|---|
committer | 2014-10-09 16:04:42 +0200 | |
commit | 262e7b39f9fe7113ef8180786e4ae6ce69125f87 (patch) | |
tree | bab6628130e6a047b8029cf56b3d9103a017be1e /plugins | |
parent | 45566f5651176359aed523b1ddb7e9e5331897f6 (diff) |
Propagating name of goal to main subgoal in cut and conversion tactics.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions