From a3a421f504e2d409f5377ef0ac66a24b93d3ab88 Mon Sep 17 00:00:00 2001 From: joneugster Date: Wed, 29 Nov 2023 15:14:00 +0100 Subject: [PATCH] fix bubblewrap script --- server/bubblewrap.sh | 6 ++++-- server/index.mjs | 4 ++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh index c4deee2..6f6cd20 100755 --- a/server/bubblewrap.sh +++ b/server/bubblewrap.sh @@ -2,8 +2,10 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) + + (exec bwrap\ - --bind ../../lean4game /lean4game \ + --bind $2 /lean4game \ --bind $1 /game \ --bind $ELAN_HOME /elan \ --bind /usr /usr \ @@ -22,6 +24,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) --unshare-uts \ --unshare-cgroup \ --die-with-parent \ - --chdir "/lean4game/server/build/bin/" \ + --chdir "/lean4game/server/.lake/build/bin/" \ ./gameserver --server /game ) diff --git a/server/index.mjs b/server/index.mjs index 00b1082..4ac9d8d 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -85,8 +85,8 @@ function startServerProcess(owner, repo) { { cwd: path.join(__dirname, "./.lake/build/bin/") }) } else { serverProcess = cp.spawn("./bubblewrap.sh", - [game_dir], - { cwd: __dirname }) + [game_dir, path.join(__dirname, '..')], + { cwd: path.join(__dirname, '..') }) } serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`)