Fix: Menu change is done just after update

htdocs/admin/menus.php

@@ -15,14 +15,13 @@
  * You should have received a copy of the GNU General Public License
  * along with this program; if not, write to the Free Software
  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
- *
- * $Id$
  */
 
 /**
         \file       htdocs/admin/menus.php
         \ingroup    core
         \brief      Page de configuration des gestionnaires de menu
+		\version	$Id$
 */
 
 require("./pre.inc.php");
@@ -75,6 +74,9 @@ if (isset($_POST["action"]) && $_POST["action"] == 'update')
 		}
 	}
 
+	// We make a header redirect because we need to change menu NOW.
+	header("Location: ".$_SERVER["PHP_SELF"]);
+	exit;
 }