Merge pull request #6767 from benz0li/update-dev-containers-7e4ed3b-2

mpilgrem · web-flow · commit 16fad02a4179 · 2025-07-19T22:00:51.000+01:00
Dev Containers: Rename 'Default'
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -1,5 +1,5 @@
 {
-  "name": "Default",
+  "name": "GHC 9.10.2 (default)",
   "build": {
     "dockerfile": "GHC.Dockerfile",
     "args": {
diff --git a/.devcontainer/ghc-9.12.2/devcontainer.json b/.devcontainer/ghc-9.12.2/devcontainer.json
@@ -1,5 +1,5 @@
 {
-  "name": "GHC 9.12.2",
+  "name": "GHC 9.12.2 (experimental)",
   "build": {
     "dockerfile": "../GHC.Dockerfile",
     "context": "..",
