diff options
Diffstat (limited to 'miniprokit.sh')
| -rwxr-xr-x | miniprokit.sh | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/miniprokit.sh b/miniprokit.sh index b911f3c..8e8af01 100755 --- a/miniprokit.sh +++ b/miniprokit.sh @@ -324,16 +324,20 @@ cmd_shell() chroot "${root}" /bin/sh printf '\nExiting...\n' - # umount sometimes complains that ${root}/dev is busy. Here's a kludge - # to try to avoid that. - sleep 1 case "$(cat "${root}/etc/proteanos_arch")" in *'-linux-'*) umount "${root}/dev/pts" umount "${root}/proc" umount "${root}/sys" - umount "${root}/dev" + while ! umount "${root}/dev"; do + # umount sometimes complains that ${root}/dev is + # busy. Here's a kludge to try to handle that. + # This is a bind mount, so we better make sure + # it gets unmounted; otherwise, `rm -Rf ${root}` + # can be painful. + sleep 1 + done ;; esac } |