Michael J Gruber <git@xxxxxxxxxxxxxxxxxxxx> writes: > Are we at a point where we can still rename the new feature at least? If > yes, and keeping everything else is mandatory, than "workspace" or > "working space" may be a serious contender for naming the new thing. I do not have a good answer to the first question, but workspace does sound like a good name for what this feature is trying to achieve.