Update create_game.md

8 months ago · 1febc51791
parent d53b57a764
commit 1febc51791
1 changed files with 1 additions and 1 deletions
--- a/doc/create_game.md
+++ b/doc/create_game.md
@ -10,7 +10,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr

 ### Running the game

-Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult the section " 5.Testing the Game Locally" below.
+Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult the section "**5. Testing the Game Locally**" below.

 ## 2. Game.lean