From 80ebb8dcdf12f32873670c8adcdd8d49ca2c7b01 Mon Sep 17 00:00:00 2001
From: Richard Hartmann <richih.mailinglist@gmail.com>
Date: Fri, 10 Feb 2012 17:38:35 +0100
Subject: [PATCH 1/1] Fix `vcsh delete`

Use rm -r instead of rmdir as the directory will _never_ be empty
---
 vcsh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vcsh b/vcsh
index 41d5ed0..a578487 100755
--- a/vcsh
+++ b/vcsh
@@ -100,7 +100,7 @@ To continue, type 'Yes, do as I say'"
 	for file in $files; do
 		rm -f $file || info "could not delete '$file', continuing with deletion"
 	done
-	rmdir "$GIT_DIR" || error "could not delete '$GIT_DIR'"
+	rm -r "$GIT_DIR" || error "could not delete '$GIT_DIR'"
 }
 
 enter() {
-- 
2.39.5