diff options
| author | Andreas Gohr <andi@splitbrain.org> | 2013-08-11 12:18:38 +0200 |
|---|---|---|
| committer | Andreas Gohr <andi@splitbrain.org> | 2013-08-11 12:18:38 +0200 |
| commit | 95905cbe48caa3de7d6d809a8f0d0cffc9df4720 (patch) | |
| tree | f90102632f52fa0e1500fead6bd085ad62eb2756 | |
| parent | 2e308c3608bea50e07aacf51b232eaedbda6eb20 (diff) | |
| download | rpg-95905cbe48caa3de7d6d809a8f0d0cffc9df4720.tar.gz rpg-95905cbe48caa3de7d6d809a8f0d0cffc9df4720.tar.bz2 | |
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.
| -rw-r--r-- | inc/html.php | 8 |
1 files 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">'. |