diff options
author | Konstantin Baranov <konstantin.baranov@workato.com> | 2020-10-26 18:02:52 -0700 |
---|---|---|
committer | Konstantin Baranov <konstantin.baranov@workato.com> | 2020-10-26 18:02:52 -0700 |
commit | 2b72da8bf95e3e1afb361f8984584bcf0524cff3 (patch) | |
tree | 49204fa30a9e8d20a9b4d0674a2bcab7a710268b /.github | |
parent | 3fd4b83fa325de5e4e49c6fdcaa95a1a3db486ed (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