add devcontainer and tasks.json

2023-06-07 14:13:09 +00:00
parent 527f977f79
commit 08d1e17286
4 changed files with 63 additions and 0 deletions
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -0,0 +1,15 @@
+{
+  "version": "2.0.0",
+  "tasks": [
+    {
+      "label": "lake: build",
+      "detail": "build lean files",
+      "type": "shell",
+      "command": "lake build",
+      "group": {
+        "kind": "build",
+        "isDefault": true
+      },
+    }
+  ]
+}