From e09c016c4c6646d3d625c172dceb06499a7cdffd Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 10 Nov 2023 11:15:53 +0100 Subject: [PATCH] Update update_game.md --- doc/update_game.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.