diff options
| author | Egor Tensin <Egor.Tensin@gmail.com> | 2018-05-23 22:57:51 +0300 |
|---|---|---|
| committer | Egor Tensin <Egor.Tensin@gmail.com> | 2018-05-23 22:57:51 +0300 |
| commit | 182cbb0c69379f27cda11e695ea68bf7dc64b59c (patch) | |
| tree | 42e967f5109dfb6594526d7e5dd9845bf8bacb58 | |
| parent | .gitconfig: add comments to git settings (diff) | |
| download | linux-home-182cbb0c69379f27cda11e695ea68bf7dc64b59c.tar.gz linux-home-182cbb0c69379f27cda11e695ea68bf7dc64b59c.zip | |
runc*: best bash practices
| -rw-r--r-- | %HOME%/.bash_utils/cxx.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/%HOME%/.bash_utils/cxx.sh b/%HOME%/.bash_utils/cxx.sh index d5ce371..438f798 100644 --- a/%HOME%/.bash_utils/cxx.sh +++ b/%HOME%/.bash_utils/cxx.sh @@ -117,7 +117,10 @@ runc() ( local build_dir build_dir="$( mktemp --directory )" - trap "$( printf -- 'popd > /dev/null && rm -rf -- %q' "$build_dir" )" 0 + local rm_build_dir + rm_build_dir="$( printf -- 'popd > /dev/null && rm -rf -- %q' "$build_dir" )" + + trap "$rm_build_dir" EXIT pushd "$build_dir" > /dev/null local output_name |