fix: Add Java feature for Prusti

MathieuSoysal · Mar 3, 2024 · 2e3db33 · 2e3db33
1 parent d4a1bee
commit 2e3db33
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -6,7 +6,8 @@
 	"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/github-cli:1": {},
+		"ghcr.io/devcontainers/features/java:1": {} // Used for Prusti
 	},
 	"customizations": {
 		"vscode": {