greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

devcontainer setup

Browse Source
This commit is contained in:
Jon Eugster
2023-09-10 13:36:53 +02:00
parent cb05a73353
commit bba96eccac
1 changed files with 5 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
.devcontainer/devcontainer.json
View File

@@ -11,12 +11,11 @@
"updateRemoteUserUID": true,
// I don't know why I need this, but I did...
"overrideCommand": true,
// TODO: `lake` and `npm install` could run simultaneously using `&`
// the only reason I didn't do it is because the output gets mixed.
"initializeCommand": "",
"onCreateCommand": "",
// "postCreateCommand": "(cd ~/lean4game && npm install) && (cd ~/game && lake update && lake exe cache get && lake build)",
// "postAttachCommand": "cd ~/lean4game && npm start",
"onCreateCommand": {
"npm_install": "(cd ~/lean4game && npm install)",
"lake_build": "(cd ~/game && lake clean && lake exe cache get && lake build)"
},
"postAttachCommand": "cd ~/lean4game && npm start",
"customizations": {
"vscode": {
"settings": {