Compare commits

..
Author SHA1 Message Date
Jon Eugster c533a635c2 Update docs 2024-01-18 13:47:08 +01:00
Jon Eugster 7114a8c4cb fix: remove tmp files after import 2024-01-15 12:15:12 +01:00
Jon Eugster b7eb15184d Merge pull request #182 from lnay/patch-1
Minor: correct error in markdown
2024-01-15 11:24:46 +01:00
Luke Naylor 892c70165a Minor: correct error in markdown 2024-01-12 21:07:19 +00:00
3 changed files with 7 additions and 11 deletions
+1 -1
View File
@@ -1,6 +1,6 @@
# Publishing games
You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple
steps.
## 1. Upload Game to github
+2 -10
View File
@@ -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
@@ -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".
+4
View File
@@ -28,3 +28,7 @@ do
#tar -xvzf $f -C games/${OWNER}/${REPO}
unzip -q -o $f -d ${OWNER}/${REPO}
done
# Delete temporary files
rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}