@Findus23 opened this Pull Request on February 10th 2019 Member

while looking into #14082, I just found this old branch.

Can everyone please check if those files are really not needed?

@tsteur commented on February 10th 2019 Member

I don't think they are needed

@diosmosis commented on February 11th 2019 Member

👍

This Pull Request was closed on February 11th 2019
Powered by GitHub Issue Mirror