index a41373dc0c9abcee9623c7635d98214cb000837d..f50097ec8c81ca59108e7cd5cc5f747edaf566db 100644 (file)
"*** PHP error information ***\n\n");
}
- if (isset($_SESSION['js']) && $_SESSION['js']==FALSE){
+ if (session::is_set('js') && session::get('js')==FALSE){
$error_collector= "<div>";
} else {
$error_collector= "