plugins/admin/PluginManager.php
changeset 524 26287ae2449d
parent 519 94214ec0871c
child 526 b2fb50d572c7
--- a/plugins/admin/PluginManager.php	Tue Apr 08 20:30:50 2008 -0400
+++ b/plugins/admin/PluginManager.php	Tue Apr 08 20:31:58 2008 -0400
@@ -253,6 +253,8 @@
           // not set, skip this plugin
           continue 2;
       }
+      // decide if it's a system plugin
+      $plugin_meta['system plugin'] = in_array($dh, $plugins->system_plugins);
       // all checks passed
       $plugin_list[$dh] = $plugin_meta;
     }