@sgiehl opened this Pull Request on January 6th 2018 Member

fixes #12394

@sgiehl commented on February 26th 2018 Member

@tsteur would you have some time for another review on this? Would be good to merge some more of the open PRs

@tsteur commented on February 26th 2018 Member

Just tested and worked. Be good to add the other comment, otherwise good to merge.

@sgiehl commented on February 26th 2018 Member

Ok. I've added the comment. Will now wait for the tests before merging...

This Pull Request was closed on February 26th 2018
Powered by GitHub Issue Mirror