From d00a2337d4ab3a19cf34f67f8dde4e4f8fed7ae1 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 9 Aug 2023 15:23:10 +0200
Subject: [PATCH] elan home dynamically

---
 NOTES.md             | 5 +++++
 server/bubblewrap.sh | 4 +++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/NOTES.md b/NOTES.md
index ee7a6a2..288e6ab 100644
--- a/NOTES.md
+++ b/NOTES.md
@@ -195,3 +195,8 @@ Activate config:
 ```
 sudo apt-get install unzip
 ```
+
+## Install bubblewrap (bwrap)
+```
+sudo apt-get install bubblewrap
+```
diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh
index 5b7efb1..7d3f10e 100755
--- a/server/bubblewrap.sh
+++ b/server/bubblewrap.sh
@@ -1,9 +1,11 @@
 #/bin/bash
 
+ELAN_HOME=$(lake env printenv ELAN_HOME)
+
 (exec bwrap\
   --ro-bind ../../lean4game /lean4game \
   --ro-bind ../../$1 /game \
-  --ro-bind ~/.elan /elan \
+  --ro-bind $ELAN_HOME /elan \
   --ro-bind /usr /usr \
   --dev /dev \
   --proc /proc \