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-11-10 11:15:53 +01:00
committed by GitHub
parent 06d9656e88
commit e09c016c4c
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/update_game.md
+1 -1
View File
@@ -10,7 +10,7 @@ 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: Then, depending on the setup you use, do one of the following:
* Dev Container: Rebuild the VSCode Devcontainer. * Dev Container: Rebuild the VSCode Devcontainer.
* Local Setup: run `lake update` (followed by `lake exe cache get` if you depend on mathlib.) * Local Setup: run `lake update -R` (followed by `lake exe cache get` if you depend on mathlib.)
* Gitpod/Codespaces: Create a fresh one * Gitpod/Codespaces: Create a fresh one
This will update `lean4game` and `mathlib` in your project to the new lean version. This will update `lean4game` and `mathlib` in your project to the new lean version.