elan home dynamically

pull/118/head
Alexander Bentkamp 3 years ago
parent dc144d1979
commit d00a2337d4

@ -195,3 +195,8 @@ Activate config:
``` ```
sudo apt-get install unzip sudo apt-get install unzip
``` ```
## Install bubblewrap (bwrap)
```
sudo apt-get install bubblewrap
```

@ -1,9 +1,11 @@
#/bin/bash #/bin/bash
ELAN_HOME=$(lake env printenv ELAN_HOME)
(exec bwrap\ (exec bwrap\
--ro-bind ../../lean4game /lean4game \ --ro-bind ../../lean4game /lean4game \
--ro-bind ../../$1 /game \ --ro-bind ../../$1 /game \
--ro-bind ~/.elan /elan \ --ro-bind $ELAN_HOME /elan \
--ro-bind /usr /usr \ --ro-bind /usr /usr \
--dev /dev \ --dev /dev \
--proc /proc \ --proc /proc \

Loading…
Cancel
Save