@sgiehl opened this Pull Request on September 10th 2017 Member

This might fix #11731

@mattab commented on November 20th 2017 Owner

@sgiehl :+1: this shouldn't hurt or cause any regression (hopefully) so I'm going to merge.

This Pull Request was closed on November 20th 2017
Powered by GitHub Issue Mirror