Skip to content

Commit

Permalink
chore: use --tmpdir
Browse files Browse the repository at this point in the history
  • Loading branch information
bollu committed Sep 19, 2024
1 parent e53b5cf commit 2cec60e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion server/bubblewrap.sh
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ if command -v bwrap >/dev/null 2>&1; then
--ro-bind "$LEAN_ROOT" /lean \
--ro-bind /usr /usr \
--dev /dev \
--bind /tmp/ /tmp/ \
--tmpfs /tmp \
--proc /proc \
--symlink usr/lib /lib\
--symlink usr/lib64 /lib64\
Expand Down

0 comments on commit 2cec60e

Please sign in to comment.