Skip to content

Commit

Permalink
Update docs
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Jan 18, 2024
1 parent 7114a8c commit c533a63
Showing 1 changed file with 2 additions and 10 deletions.
12 changes: 2 additions & 10 deletions doc/running_locally.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@

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.

There are several options to play a game locally:

1. VSCode Dev Container: needs `docker` installed on your machine
Expand Down Expand Up @@ -36,16 +38,6 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
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.

### Errors

* 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
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.

## 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".
Expand Down

0 comments on commit c533a63

Please sign in to comment.