aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-09-07 16:56:34 +0200
committerGaëtan Gilbert2017-11-25 14:18:35 +0100
commitc93d5094bff73498ec8fc02837e16cc5ce9103b6 (patch)
treebed26813cdb09b9c01042b984dbc494eb48e012e /API/API.mli
parente6c87412d70b71daaf417bd4b8e4ae6f1f28515b (diff)
Make restrict_universe_context stronger.
This fixes BZ#5717. Also add a test and fix a changed test.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions