Fix link references

doc/create_game.md

@@ -236,7 +236,7 @@ Most important for game development are probably the `Hints`.
 The hints will be displayed whenever the player's current goal matches the goal the hint is
 placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.
 
-Read [More about Hints](doc/hints.md) for how they work and what the options are.
+Read [More about Hints](hints.md) for how they work and what the options are.
 
 ### 6. e) Extra: Images
 You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
@@ -248,11 +248,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the
 
 ## 7. Update your game
 
-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](doc/update_game.md).
+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
 
-To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
+To publish your game on the official server, see [Publishing a game](publish_game.md)
 
 There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
 

doc/running_locally.md

@@ -2,7 +2,7 @@
 
 The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
 
-Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected.
+Please also consult the [Troubleshooting Collection](troubleshoot.md), where some known pitfalls are collected.
 
 There are several options to play a game locally:
 
@@ -33,14 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
 
     * The first start will take a while, ca. 2-15 minutes. After the first
       start this should be very quickly.
-    * Once built, you can open http://localhost:3000 in your browser. which should load the game.
+    * Once built, you can open http://localhost:3000 in your browser, which should load the game.
 
 3.  **Editing Files** *(everytime)*:<br/>
     After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
 
 ## Codespaces
 
-You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
+You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
 
 Note: You have to wait until npm started properly, which might take a good while.
 

doc/server.md

@@ -6,7 +6,7 @@ In order to set up the server to allow imports, one needs to create a
 repos will suffice.
 
 You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
-with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if
+with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if
 you're using `pm2`
 
 Then people can call:
@@ -24,5 +24,5 @@ where you replace:
 
 ## data management
 Everything downloaded remains in the folder `lean4game/games`.
-the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
+The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
 The other folders should only contain the built lean-games, sorted by owner and repo.

doc/troubleshoot.md

@@ -3,11 +3,11 @@
 Here are some issues experienced by users.
 
 # VSCode Dev-Container
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
+* If you don't get the pop-up, you might have disabled them, and you can reenable it by
   running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
 * If the starting the container fails, in particular with a message `Error: network xyz not found`,
   you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
   container. (this will again take some time)
 * On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.