aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-11-21 16:42:42 +0100
committerGaëtan Gilbert2017-12-14 19:17:49 +0100
commit30746e6a9a3296c1aacb2fc03e1c16014232219f (patch)
treef3390677c41221e01cce72543f74c8984e6eec6a /API
parentf9b715c4ea07d6ecfece7f28e4d25f3dcab01158 (diff)
Deprecate dead code option Congruence Depth.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions