plugins/admin/PluginManager.php
changeset 844 7549f2880c32
parent 812 68060328e9c6
child 869 58bc29c14a4d
--- a/plugins/admin/PluginManager.php	Thu Feb 26 01:07:32 2009 -0500
+++ b/plugins/admin/PluginManager.php	Thu Feb 26 01:27:23 2009 -0500
@@ -330,6 +330,27 @@
     return true;
   }
   
+  // Sort so that system plugins come last
+  ksort($plugin_list);
+  $plugin_list_sorted = array();
+  foreach ( $plugin_list as $filename => $data )
+  {
+    if ( !$data['system plugin'] )
+    {
+      $plugin_list_sorted[$filename] = $data;
+    }
+  }
+  ksort($plugin_list_sorted);
+  foreach ( $plugin_list as $filename => $data )
+  {
+    if ( $data['system plugin'] )
+    {
+      $plugin_list_sorted[$filename] = $data;
+    }
+  }
+  
+  $plugin_list =& $plugin_list_sorted;
+  
   //
   // Not a JSON request, output normal HTML interface
   //