diff --git a/lib/deprecatedlib.php b/lib/deprecatedlib.php index b58d1ee69bb..6301a5d4ff3 100644 --- a/lib/deprecatedlib.php +++ b/lib/deprecatedlib.php @@ -105,17 +105,21 @@ function session_kill_user($userid) { \core\session\manager::kill_user_sessions($userid); } -/** - * Session garbage collection - * - verify timeout for all users - * - kill sessions of all deleted users - * - kill sessions of users with disabled plugins or 'nologin' plugin - * - * @deprecated since 2.6 - */ -function session_gc() { - debugging('session_gc() is deprecated, use \core\session\manager::gc() instead', DEBUG_DEVELOPER); - \core\session\manager::gc(); +// PHP 5.6 includes session_gc(), we cannot define it any more. +if (!function_exists('session_gc')) { + /** + * Session garbage collection + * - verify timeout for all users + * - kill sessions of all deleted users + * - kill sessions of users with disabled plugins or 'nologin' plugin + * + * @deprecated since 2.6 + */ + function session_gc() + { + debugging('session_gc() is deprecated, use \core\session\manager::gc() instead', DEBUG_DEVELOPER); + \core\session\manager::gc(); + } } /**