+
+ // Extension id
+ $EXT_DUMMY['ext_id'][$name] = $EXT_DUMMY['ext_id'][$k];
+ $id = $EXT_DUMMY['ext_id'][$name];
+ unset($EXT_DUMMY['ext_id'][$k]);
+
+ // Add ext name
+ $EXT_NAMES[$id] = $name;
+
+ // Add deprecated flag (defaults to "not deprecated")
+ $EXT_DUMMY['ext_deprecated'][$name] = "N";
+
+ // Mark it as active extension
+ $GLOBALS['cache_array']['active_extensions']['$name'] = $EXT_DUMMY['ext_keep'][$k];