diff options
author | 2015-02-19 16:35:42 +0100 | |
---|---|---|
committer | 2015-02-24 16:37:04 +0100 | |
commit | 2f41d8e976621b907925546a192e90e60f0e580b (patch) | |
tree | c6cad6b836d9d92cffac90058f98e500559e72da /plugins | |
parent | 50edb9bb8d43b190996d1d85a2bfd95f52b2db19 (diff) |
Refactoring in [Constr].
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions