while ( $error !== false ) {
if ( preg_match( '/^line (\d+)/', $error, $m ) ) {
$lineNum = intval( $m[1] );
$badLines[$lineNum] = true;
$out .= Html::rawElement( 'li', null,
while ( $error !== false ) {
if ( preg_match( '/^line (\d+)/', $error, $m ) ) {
$lineNum = intval( $m[1] );
$badLines[$lineNum] = true;
$out .= Html::rawElement( 'li', null,