diff --git a/doc/update_game.md b/doc/update_game.md index f75d0eb..1a18d58 100644 --- a/doc/update_game.md +++ b/doc/update_game.md @@ -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: * 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 This will update `lean4game` and `mathlib` in your project to the new lean version.