Move settings to toolbox#4041

nicolasstucki merged 1 commit intoscala:masterscala/scala3:masterfrom

dotty-staging:move-settings-to-toolboxdotty-staging/dotty:move-settings-to-toolboxCopy head branch name to clipboard