diff --git a/config/tools/rm.pl b/config/tools/rm.pl index 83f54571a..8a5ad222c 100755 --- a/config/tools/rm.pl +++ b/config/tools/rm.pl @@ -22,6 +22,10 @@ foreach $arg ( @ARGV ) { rmdir ($arg) or die "Cannot delete $arg"; } + if (-d $arg) + { + die "Failed to delete $arg"; + } } else {