diff options
| -rw-r--r-- | src/session.sh | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/session.sh b/src/session.sh index 32400ce..c4a9b08 100644 --- a/src/session.sh +++ b/src/session.sh @@ -25,6 +25,7 @@ session_plat= session_mountdir= session_atexit= session_sigs= +_session_es= _session_mount() { @@ -66,6 +67,11 @@ _session_umount() session_end() { + if [ ! -d "${session_root}/prokit/sessions/${session_id}" ]; then + # Session already ended by signal. No need for further cleanup. + return 0 + fi + trap : ${session_sigs} ${session_atexit} @@ -106,7 +112,7 @@ _session_handle_sig() session_end - exit $((128 + ${sig})) + _session_es=$((128 + ${sig})) } _session_set_sigs() @@ -207,6 +213,8 @@ session_exec() local args= local session_dir= + _session_es=0 + args='' for arg in "${@}"; do arg="'$(printf '%s\n' "${arg}" | sed "s/'/'\\\\''/g")'" @@ -216,5 +224,5 @@ session_exec() chroot "${session_root}" /bin/sh -c "cd ${session_dir}; ${args}" || \ return ${?} - return 0 + return ${_session_es} } |