diff options
author | Wynn Wolf Arbor | 2020-03-23 14:37:29 +0100 |
---|---|---|
committer | Wynn Wolf Arbor | 2020-03-23 14:37:29 +0100 |
commit | 8bf9fb6f0a13a0d7f72e88c5a06905bdfd6c300f (patch) | |
tree | e82fd380df5b63241c823a235f29e59baf9279ea /Makefile | |
parent | 110bf234790288036f208889cd9d5fd967993c38 (diff) | |
download | kern-8bf9fb6f0a13a0d7f72e88c5a06905bdfd6c300f.tar.gz |
Check whether /boot is already mounted
This commit adds code to check whether /boot is mounted or not, and will
skip the mount command if the path is already mounted. This will fix an
issue where the script exited prematurely if /boot was already present,
as the mount command failed and we use `set -e'.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions