From 95905cbe48caa3de7d6d809a8f0d0cffc9df4720 Mon Sep 17 00:00:00 2001
From: Andreas Gohr <andi@splitbrain.org>
Date: Sun, 11 Aug 2013 12:18:38 +0200
Subject: make extension manager the default plugin

This moves the old plugin manager down to the "other" plugins. It should
probably be removed when when we decide the new one is good to go.
---
 inc/html.php | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/inc/html.php b/inc/html.php
index 96c4eaa1a..00b929c75 100644
--- a/inc/html.php
+++ b/inc/html.php
@@ -1710,12 +1710,12 @@ function html_admin(){
         }
         unset($menu['acl']);
 
-        if($menu['plugin']){
+        if($menu['extension']){
             ptln('  <li class="admin_plugin"><div class="li">'.
-                    '<a href="'.wl($ID, array('do' => 'admin','page' => 'plugin')).'">'.
-                    $menu['plugin']['prompt'].'</a></div></li>');
+                    '<a href="'.wl($ID, array('do' => 'admin','page' => 'extension')).'">'.
+                    $menu['extension']['prompt'].'</a></div></li>');
         }
-        unset($menu['plugin']);
+        unset($menu['extension']);
 
         if($menu['config']){
             ptln('  <li class="admin_config"><div class="li">'.
-- 
cgit v1.2.3