diff options
Diffstat (limited to 'make/valgrind-wrap')
| -rwxr-xr-x | make/valgrind-wrap | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/make/valgrind-wrap b/make/valgrind-wrap deleted file mode 100755 index 40785bf1..00000000 --- a/make/valgrind-wrap +++ /dev/null @@ -1,10 +0,0 @@ -#!/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 |