diff --git a/tools/bin/erase b/tools/bin/erase new file mode 100755 index 000000000..89ca5c097 --- /dev/null +++ b/tools/bin/erase @@ -0,0 +1,9 @@ +#!/bin/sh +if test $# = 0; then +echo 'usage: erase ' +fi +file=$1 +erased_dir=$HOME/erased +mv -f $file erased_dir +cvs remove $file +