if ( !session_is_registered('prefs_are_cached') ||
!isset( $prefs_cache) ||
!is_array( $prefs_cache) ||
- substr( phpversion(), 0, 3 ) == '4.1' ) {
+ substr( phpversion(), 0, 3 ) == '4.1' ||
+ substr( phpversion(), 0, 3 ) == '4.2' ) {
$prefs_are_cached = false;
$prefs_cache = array();
}