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

Update update_game.md

Browse Source
This commit is contained in:
Jon Eugster
2023-12-18 16:20:26 +01:00
committed by GitHub
parent c4f4dbdc6b
commit 7882958f54
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/update_game.md
+3 -3
View File
@@ -9,8 +9,8 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
Then, depending on the setup you use, do one of the following:
* Dev Container: Rebuild the VSCode Devcontainer.
* Local Setup: in your game's folder run the following:
* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
* **Local Setup**: in your game's folder run the following:
```
lake update -R
lake build
@@ -24,7 +24,7 @@ Then, depending on the setup you use, do one of the following:
npm install
```
where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
* Gitpod/Codespaces: Create a fresh one
* **Gitpod/Codespaces**: Create a fresh one
This will update your game (and the mathlib version you might be using) to the new lean version.