Die if rmtree fails.

2001-10-01 17:45:09 +00:00
parent d4107b4900
commit ec8a33ea5b
1 changed files with 4 additions and 0 deletions
--- 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
 	{