mirror
/
mongo
mirror of https://github.com/mongodb/mongo
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

SERVER-112732: Use a better name for the devcontainer container name (#43100) 

GitOrigin-RevId: 56f5f16b016c1f008add73cfad6a27ccdad9bc6b
This commit is contained in:
Eric Lavigne 2025-10-25 01:56:50 -04:00 committed by MongoDB Bot
parent 3e02343dd6
commit 9cfa07acb4
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.devcontainer/devcontainer.json
View File

@ -1,5 +1,8 @@
{
"name": "MongoDB Development Container",
"runArgs": [
"--name=mongo-dev-${containerWorkspaceFolderBasename}-${devcontainerId}"
],
"build": {
"dockerfile": "./Dockerfile",
"context": "..",