From 28a7c65db28dadba2e557eaa477d4762b269a4d0 Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Thu, 30 Nov 2023 19:26:42 +0100
Subject: [PATCH] update doc, including #148

---
 .gitignore         |  1 +
 doc/update_game.md | 28 ++++++++++++++++++++--------
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/.gitignore b/.gitignore
index f6fa519..9508154 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 node_modules
+games/
 client/dist
 games/
 server/.lake
diff --git a/doc/update_game.md b/doc/update_game.md
index 2c9afe2..8fcb037 100644
--- a/doc/update_game.md
+++ b/doc/update_game.md
@@ -12,12 +12,22 @@ Then, depending on the setup you use, do one of the following:
 * Dev Container: Rebuild the VSCode Devcontainer.
 * Local Setup: run
   ```
-  npm install
   lake update -R
+  lake build
   ```
+  in your game folder.
+
+  * Additionally, if you have a local copy of the server `lean4game`,
+    you should update this one to the matching version, too:
+    ```
+    git fetch
+    git checkout {VERSION_TAG}
+    npm install
+    ```
+    where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
 * Gitpod/Codespaces: Create a fresh one
 
-This will update `lean4game` and `mathlib` in your project to the new lean version.
+This will your game (and the mathlib version you might be using) to the new lean version.
 
 ## Newest developing setup
 
@@ -28,14 +38,16 @@ anymore, you will need to copy the relevant files from the [GameSkeleton](https:
 The relevant files are:
 
 ```
+.devcontainer/
+.docker/
+.github/
+.gitpod/
+.vscode/
 lakefile.lean
-.devcontainer/**
-.docker/**
-.gitpod
-.vscode/**
 ```
 
-simply copy them from the `GameSkeleton` into your game.
+simply copy them from the `GameSkeleton` into your game and proceed as above,
+i.e. `lake update -R && lake build`.
 
 (Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
-where you need to add any dependencies of your game.)
+where you need to add any dependencies of your game, or remove mathlib if you don't need it.)