I wouldn't change the setting name, at least not in this PR, it just makes for a lot of noise thats irrelevant to the PR itself. @codebrainz can look it up :) If you really want to change it make it a separate change.

And anyway I thought you didn't need it any more, only the project load and close?

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.