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-30 19:32:38 +01:00
committed by GitHub
parent 7f91ae7da8
commit 622e9d3897
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
@@ -32,7 +32,7 @@ This will your game (and the mathlib version you might be using) to the new lean
## Newest developing setup
There are a few files in your game repository which are used for the developing setup
(dev container/codespaces/gitpod). If you need to update your're developing setup, for example because it doesn't work
(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
The relevant files are: