update npm deps

bump npm dependencies
Update troubleshoot.md
2024-02-23 18:58:15 +01:00 · 2024-02-23 18:58:06 +01:00 · 2024-02-16 10:57:02 +01:00
3 changed files with 1732 additions and 2350 deletions
@@ -2,6 +2,15 @@

 Here are some issues experienced by users.

+- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
+  ```
+  cd [THE PROJECT]
+  rm -rf .lake/
+  lake update -R
+  lake build
+  ```
+  If you experience problems related to Lean or lake, you should first try to reset it this way.
+
 # VSCode Dev-Container
 * If you don't get the pop-up, you might have disabled them, and you can reenable it by
  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
@@ -28,7 +28,7 @@
    "debounce": "^1.2.1",
    "express": "^4.18.2",
    "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+    "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
    "octokit": "^3.1.2",
    "path-browserify": "^1.0.1",
    "react": "^18.2.0",
Author	SHA1	Message	Date
Jon Eugster	d689c7ec86	update npm deps	2024-02-23 18:58:15 +01:00
Jon Eugster	16c979a6c2	bump npm dependencies	2024-02-23 18:58:06 +01:00
Jon Eugster	698a88c545	Update troubleshoot.md	2024-02-16 10:57:02 +01:00