From de1ff4fadcfb112c8e7f1150ce9664978e7b4985 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 10 Apr 2024 16:12:35 +0200 Subject: [PATCH] Update create_game.md --- doc/create_game.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/create_game.md b/doc/create_game.md index 3a17fc0..589fc1d 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -242,7 +242,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md). -## 8. Publish your game +## 8. Add translation + +See [Translating a game](translate.md). + +## 9. Publish your game To publish your game on the official server, see [Publishing a game](publish_game.md)