microsoft / microsoft/vscode-remote-release

Always install extensions to support mounting the home folder

Open
#5,229 15 comments 8 reactions 1 assignee View on GitHub

@chrmarti is already working on this.

Since Jun 21, 2021.

containers feature-request
Dominant language
Dockerfile
Stars
4.2k
Forks
470
Avg merge
1d 1h
Merged PRs (30d)
1

Description

Issue type: feature request

Description

We use dev container and we mount local folder from docker host into the user's home folder inside the container (eg. '/root/`).

The file /root/.vscode-server/data/Machine/.installExtensionsMarker is created every time we start our dev container and that prohibits us to install additional extensions. In case the file exist no extension is installed to prevent altering the container.

I did not see any issue regarding extension installation so I do not understand why the .installExtensionsMarker file is not deleted during dev container startup.

Actual behavior

We need to remove the marker file with a script using the initializeCommand or the postCreateCommand to allow new extension to be installed.

Expected

The extensions shall be installed on the mounted home folder in the following case:

  • we extend the list of extensions in the .devcontainer.json (eg.: by updating the git repository),
  • we add some extension manually.
VSCode:

Version: 1.57.0 (user setup)
Commit: b4c1bd0a9b03c749ea011b06c6d2676c8091a70c
Date: 2021-06-09T17:18:42.354Z
Electron: 12.0.9
Chrome: 89.0.4389.128
Node.js: 14.16.0
V8: 8.9.255.25-electron.0
OS: Windows_NT x64 10.0.18363

Original topic from a different issue

@neuromechanist It looks like /root/.vscode-server-insiders/data/Machine/.installExtensionsMarker already existed (and we therefore skipped the extension install). Did you mount anything there or a parent folder?

Originally posted by @chrmarti in https://github.com/microsoft/vscode-remote-release/issues/3975#issuecomment-723872103

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.