From fee1f0601a121ffb504cc946c617c6369862e4ef Mon Sep 17 00:00:00 2001 From: DarkWiiPlayer Date: Wed, 18 Sep 2019 14:31:20 +0200 Subject: [PATCH] Fix scratch bash script --- bin/scratch | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/bin/scratch b/bin/scratch index 2d4cad6..e61ee97 100755 --- a/bin/scratch +++ b/bin/scratch @@ -1,9 +1,11 @@ #!/bin/bash export scratch=$(mktemp -p /dev/shm -d -t tmp.XXXXXXXXXX) + function finish { - echo "Deleting $scratch..." rm -rf "$scratch" } + trap finish EXIT -trap finish TERM -exec bash --init-file <(echo "source ~/.bashrc; pushd $scratch > /dev/null") +trap finish SIGTERM + +bash --init-file <(echo "source ~/.bashrc; pushd $scratch > /dev/null")