diff -r becbbc7f5b72 -r ae135a73e338 scripts/functions
--- a/scripts/functions	Mon Jan 12 18:54:34 2009 +0000
+++ b/scripts/functions	Mon Jan 12 21:35:23 2009 +0000
@@ -242,6 +242,13 @@
     return 0
 }
 
+# Removes one or more directories, even if it is read-only
+# Usage: CT_DoForceRmdir dir [...]
+CT_DoForceRmdir() {
+    CT_DoExecLog ALL chmod -R u+w "${@}"
+    CT_DoExecLog ALL rm -rf "${@}"
+}
+
 # Echoes the specified string on stdout until the pipe breaks.
 # Doesn't fail
 # $1: string to echo