From 1febc517919e0ff998853addf97add3ccabcc60b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 13 Jun 2024 11:46:01 +0200 Subject: [PATCH] Update create_game.md --- doc/create_game.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/create_game.md b/doc/create_game.md index b26a06d..8d2c3f7 100644 --- 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