From 7882958f54a124c74b1e61d6e55689906db551c4 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 18 Dec 2023 16:20:26 +0100 Subject: [PATCH] Update update_game.md --- doc/update_game.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/update_game.md b/doc/update_game.md index ff4113d..1a48fbc 100644 --- a/doc/update_game.md +++ b/doc/update_game.md @@ -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.