phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update troubleshoot.md

Browse Source
This commit is contained in:
Jon Eugster
2024-02-16 10:57:02 +01:00
committed by GitHub
parent 3b660c5185
commit 698a88c545
1 changed files with 9 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/troubleshoot.md
+9
View File
@@ -2,6 +2,15 @@
Here are some issues experienced by users. 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 # VSCode Dev-Container
* If you don't get the pop-up, you might have disabled them, and you can reenable it by * 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. running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.