session destroy

diff --git a/install/save.php b/install/save.php
index 801c2a1ab7a66902e22255c47d8558d4be743996..acb8666bc4ee2ec94735985d67605226e8f5f8a6 100644 (file)
--- a/install/save.php
+++ b/install/save.php
@@ -379,10 +379,24 @@ if (!$db)
                        display_error("The configuration file $config_filename is not writable. Change its permissions so it is, then re-run step 4.");
        }
 }
-
+/*
 session_unset();
 session_destroy();
 $_SESSION = array();
+*/
+session_start();
+$_SESSION = array();
+// If it's desired to kill the session, also delete the session cookie.
+// Note: This will destroy the session, and not just the session data!
+if (ini_get("session.use_cookies")) {
+    $params = session_get_cookie_params();
+    setcookie(session_name(), '', time() - 42000,
+        $params["path"], $params["domain"],
+        $params["secure"], $params["httponly"]
+    );
+}
+// Finally, destroy the session.
+session_destroy();
 header("Location: ".$path_to_root."/index.php");
 exit();