Ticket #25229: plugin-editor.php.patch

wp-admin/plugin-editor.php

@@ -94 +94 @@
 
         // List of allowable extensions
         $editable_extensions = array('php', 'txt', 'text', 'js', 'css', 'html', 'htm', 'xml', 'inc', 'include');
+
+        /**
+         * File type extensions editable in the plugin editor.
+         *
+         * If a plugin ships with files with other file extensions than the default
+         * and wants the user to be able to edit those it should use this filter.
+         *
+         * @since 2.8
+         *
+         * @param array $editable_extensions Currently editable extensions.
+         */
         $editable_extensions = (array) apply_filters('editable_extensions', $editable_extensions);
 
         if ( ! is_file($real_file) ) {