From 6249cf7c84b9867834f2979e58693835519d3895 Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Mon, 7 Sep 2026 13:33:59 +0200 Subject: [PATCH 1/2] Add devcontainer CLI instructions Signed-off-by: Christoph Knittel --- CONTRIBUTING.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 2117cbeffb..08072aa5c0 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -118,6 +118,21 @@ Run the `Dev Containers: Rebuild and Reopen in Container` action to get started. You can also open this dev container with [GitHub Codespaces](https://github.com/features/codespaces/). +Alternatively, install the [Dev Container CLI](https://github.com/devcontainers/cli) through npm: + +```sh +npm install -g @devcontainers/cli +``` + +Then create the development container and open a shell in it: + +```sh +devcontainer up --workspace-folder . +devcontainer exec --workspace-folder . zsh +``` + +Use the Dev Container tooling rather than building `.devcontainer/Dockerfile` directly. The tooling installs the features declared in `devcontainer.json`, including Node.js, and runs the post-create command. A plain `docker build` does not apply these features or lifecycle commands. + ## Building the Compiler Main targets: From 2cf5c94e4a8aa7a14c94d64e2e76c19a1631fcc7 Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Mon, 7 Sep 2026 13:52:35 +0200 Subject: [PATCH 2/2] Ignore local devcontainer lockfile Signed-off-by: Christoph Knittel --- .devcontainer/.gitignore | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 .devcontainer/.gitignore diff --git a/.devcontainer/.gitignore b/.devcontainer/.gitignore new file mode 100644 index 0000000000..83cf9abb0d --- /dev/null +++ b/.devcontainer/.gitignore @@ -0,0 +1,2 @@ +devcontainer-lock.json +