Allow pre tags in comments

pre-tags-in-comments.php

<?php
/**
 * Allow 'pre' tags in comments.
 * This is not by default allowed for users who cannot publish 'unfiltered_html'.
 * Maybe this should go in WP-MarkDown?
 *
*/
add_filter( 'wp_kses_allowed_html', 'myprefix_allow_pre_tags_in_comments', 10, 2 );
function myprefix_allow_pre_tags_in_comments( $tags, $context ){
	if( 'pre_comment_content' == $context ){
		$tags['pre'] = array();
	}
	return $tags;
}
?>