From c3cbf1bd2c0a094e0206d823afd16880962704ad Mon Sep 17 00:00:00 2001 From: "Janet B. Anderson" Date: Fri, 8 Jun 2001 20:36:54 +0000 Subject: [PATCH] Die if rmtree fails. --- configure/tools/rm.pl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/configure/tools/rm.pl b/configure/tools/rm.pl index 83f54571a..8a5ad222c 100755 --- a/configure/tools/rm.pl +++ b/configure/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 {