From c706b66af163205252a1543437b4c23575286075 Mon Sep 17 00:00:00 2001 From: joneugster Date: Tue, 14 Nov 2023 21:52:23 +0100 Subject: [PATCH] update doc to use -K option for local setup --- client/src/index.tsx | 9 --------- doc/running_locally.md | 8 ++++---- 2 files changed, 4 insertions(+), 13 deletions(-) diff --git a/client/src/index.tsx b/client/src/index.tsx index 85c6c83..9367f4c 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -15,15 +15,6 @@ import { monacoSetup } from 'lean4web/client/src/monacoSetup' monacoSetup() -// // Do not show the landing page in the dev-container context -// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? { -// path: "/", -// loader: () => redirect("/g/local/game") -// } : { -// path: "/", -// element: , -// } - // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to // `/g/local/game`. This is used for the devcontainer setup diff --git a/doc/running_locally.md b/doc/running_locally.md index 9ee9db5..0497f18 100644 --- a/doc/running_locally.md +++ b/doc/running_locally.md @@ -113,12 +113,12 @@ This takes a little time. Eventually, the game is available on http://localhost: ## Modifying the GameServer -When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export LEAN4GAME=local` inside your local game before building it: +When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`: ```bash cd NNG4 -export LEAN4GAME=local -lake update -R +lake update -R -Klean4game.local lake build ``` -This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`. +This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, you can the local copy of the edit `GameServer` in `../lean4game` and +`lake build` will then directly use this modified copy to build your game.