summaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorKonstantin Baranov <konstantin.baranov@workato.com>2020-10-26 18:02:52 -0700
committerKonstantin Baranov <konstantin.baranov@workato.com>2020-10-26 18:02:52 -0700
commit2b72da8bf95e3e1afb361f8984584bcf0524cff3 (patch)
tree49204fa30a9e8d20a9b4d0674a2bcab7a710268b /.github
parent3fd4b83fa325de5e4e49c6fdcaa95a1a3db486ed (diff)
Allow overriding mount options for /dev and /dev/pts
This is useful to optionally set /dev ro,noexec. Treat /dev and /dev/pts the same as /proc and /sys. Make sure the Type is right though. Many config.json snippets on the Internet suggest /dev is tmpfs, not devtmpfs.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions