diff --git a/mach/install b/mach/install index 0358e56f4..16dcaa9c3 100755 --- a/mach/install +++ b/mach/install @@ -1,7 +1,12 @@ MACH=`(cd .. ; basename \`pwd\`)` -if cp $1 ../../../lib/${MACH}/$1 +if cp $1 ../../../lib/${MACH}/$1 >/dev/null 2>&1 || + { rm -f ../../../lib/${MACH}/$1 >/dev/null 2>&1 && + cp $1 ../../../lib/${MACH}/$1 >/dev/null 2>&1 + } then set - ranlib ../../../lib/${MACH}/$1 >/dev/null 2>&1 exit 0 +else + echo Sorry, can not create "lib/${MACH}/$1". fi