Merge pull request #1353 from zed-industries/fix-init-user-settings

Avoid copying all default settings to initial user settings
c90fe31249Max Brunsfeld committed on 7/14/2022, 12:31:10 AM· committed by GitHubparents66cd4b38292ba1
3 files changedLine totals unavailable