To be merged in a few days.
LGTM. Feel free to merge when appropriate.
Commit d166dfdb fixes this pull-request
Pull-Request has been merged by kparal
To be merged in a few days.