rename workspace

[haneenmahd]

Currently, there is no way you could edit the names of a workspace.
It is hard to remember those freaky names all the time.

[ghuntley]

I agree the current naming system needs to be revisited. The current proposal is to change the behaviour to generate names using org followed by the repo-name. Would this help?

e.g.: gitpod_io-gitpod-12rpnh3r

See #3908 and #4129 (comment)

Personally, I would be hesitant to advocate for a way to rename workspaces because the lifecycle of workspaces should be short lived with a workspace created for each task then thrown away. This video further explains our recommended workflow https://www.gitpod.io/screencasts/fresh-dev-environments-for-each-new-task

[svenefftinge]

this is a duplicate of #4857