From b0fd03f57117452b0dbea4b469b2db22a9fa9207 Mon Sep 17 00:00:00 2001
From: Matt Pass <matt@mattpass.com>
Date: Wed, 25 Jun 2014 12:49:29 +0100
Subject: [PATCH] Don't die if dir isn't deleted

If we fail to rmdir (perhaps a permission problem), don't die. This
silently continues and does leave empty folders behind, but stops things
from breaking until the solution is really found.
---
 lib/plugins-manager.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/plugins-manager.php b/lib/plugins-manager.php
index b6eda70..b103999 100644
--- a/lib/plugins-manager.php
+++ b/lib/plugins-manager.php
@@ -174,7 +174,7 @@ function deletePlugin($dir) {
                 chdir('.');
                 deletePlugin($dir.$file.'/');
                 if(is_dir($dir.$file)) {
-			rmdir($dir.$file) or DIE("<span style='color: #fff'>couldn't delete dir: $dir$file</span><br />");
+			rmdir($dir.$file);// or DIE("<span style='color: #fff'>couldn't delete dir: $dir$file</span><br />");
 		}
             }
             else