From cb33fce236b864648109014e2d2860e3811950cf Mon Sep 17 00:00:00 2001 From: Mathieu Soysal Date: Wed, 11 Dec 2024 12:24:48 +0000 Subject: [PATCH] Remove Java feature from devcontainer configuration --- .devcontainer/devcontainer.json | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index e9a1070..c4fa1a1 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -6,8 +6,7 @@ "image": "mcr.microsoft.com/devcontainers/rust:1-1-bullseye", "features": { "ghcr.io/devcontainers/features/rust:1": {}, - "ghcr.io/devcontainers/features/github-cli:1": {}, - "ghcr.io/devcontainers/features/java:1": {} // Used for Prusti + "ghcr.io/devcontainers/features/github-cli:1": {} }, "customizations": { "vscode": { @@ -40,8 +39,7 @@ "ZhangYue.rust-mod-generator", "usernamehw.errorlens", "seatonjiang.gitmoji-vscode", - "github.vscode-github-actions", - "viper-admin.prusti-assistant" + "github.vscode-github-actions" ] }, "codespaces": {