Also clean PHP 5.5 opcache

diff --git a/lib/util.php b/lib/util.php
index 2586ad28320eaefc06174fd41ba8bba3b58d34bc..1f666a5e37fd4df3b141f815090722b11f89df04 100755 (executable)
--- a/lib/util.php
+++ b/lib/util.php
@@ -871,6 +871,10 @@ class OC_Util {
                if (function_exists('xcache_clear_cache')) {
                        xcache_clear_cache(XC_TYPE_VAR, 0);
                }
+               // Opcache (PHP >= 5.5)
+               if (function_exists('opcache_reset')) {
+                       opcache_reset();
+               }
        }
 
        /**