_('Configuration cache stale.'), 'body'=>_('Your configuration has been automatically refreshed.'), 'type'=>'info')); $config_file = CONFDIR.'config.php'; check_config($config_file); } else { # Sanity check, specially when upgrading from a previous release. if (isset($_SESSION['cache'])) foreach (array_keys($_SESSION['cache']) as $id) if (isset($_SESSION['cache'][$id]['tree']['null']) && ! is_object($_SESSION['cache'][$id]['tree']['null'])) unset($_SESSION['cache'][$id]); } } # If we came via index.php, then set our $config. if (! isset($_SESSION[APPCONFIG]) && isset($config)) $_SESSION[APPCONFIG] = $config; } /** * Stops the current session. */ function pla_session_close() { @session_write_close(); } ?>