diff options
Diffstat (limited to 'make/valgrind-wrap')
-rwxr-xr-x | make/valgrind-wrap | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/make/valgrind-wrap b/make/valgrind-wrap new file mode 100755 index 00000000..40785bf1 --- /dev/null +++ b/make/valgrind-wrap @@ -0,0 +1,10 @@ +#!/bin/sh +set -e +pwd +dir=$(dirname $1) +if [ ! -x $dir/exec-z ]; then + ln -f make/exec-z $dir/exec-z +fi +mkdir -p $dir/z +mv $1 $dir/z +ln -f $dir/exec-z $1 |