aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-26 22:48:20 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-26 22:48:20 +0200
commit74716b32ce4d37a1210dfff659870995dda99e10 (patch)
treec09600ff37b5e7dcc956bb88c6125ec1390a0ceb /dev
parentb98ae49d282f73343c1950e960f4b3bc7c28de70 (diff)
parent8ab4f8f76958d2603858ad3e4073be61ad38d113 (diff)
Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions