@tsteur opened this Pull Request on July 14th 2020 Member

Just in case some plugins use custom preference names then they can still use them by declaring them in the settings.

This Pull Request was closed on July 20th 2020
Powered by GitHub Issue Mirror