Ticket #9393: 9393-plugin-editor.diff

wp-admin/plugin-editor.php

@@ -174 +174 @@
                 <input type="hidden" name="file" value="<?php echo $file ?>" />
                 <input type="hidden" name="plugin" value="<?php echo $plugin ?>" />
                 </div>
-                <?php if ( count( $functions ) ) : ?>
+                <?php if ( isset( $functions ) ) : ?>
                 <div id="documentation"><label for="docs-list">Documentation:</label> <?php echo $docs_select ?> <input type="button" class="button" value=" <?php _e( 'Lookup' ) ?> " onclick="if ( '' != jQuery('#docs-list').val() ) { window.open( 'http://api.wordpress.org/core/handbook/1.0/?function=' + escape( jQuery( '#docs-list' ).val() ) + '&locale=<?php echo urlencode( get_locale() ) ?>&version=<?php echo urlencode( $wp_version ) ?>&redirect=true'); }" /></div>
                 <?php endif; ?>
 <?php if ( is_writeable($real_file) ) : ?>