Gitpod: Unable to add extension to user and repository at the same time

[Kreyren]

Describe the bug

It is not possible to add an extension for the end-user and for the repository at the same time.

This is required in a case like shellcheck where end-user might want to have this extension installed as user and also to add it into the repository

[jankeromnes]

@Kreyren Good point. As a workaround, can you install it for a project, then copy the .gitpod.yml entry, then open a different repository, and install it for user, and then add the copied entry to .gitpod.yml?

[Kreyren]

@jankeromnes I've just downloaded the extension and drag-and-dropped them into the both as workaround, but it's pretty annoying especially when i am doing this for every repository~

[jankeromnes]

I would say this is a duplicate of #1615 (because fixing #1615 will allow installing an extension at both user- and project-level -- I don't think we want a specific option that says "install in both at the same time" because that seems like a fringe use case)