e96a21631b
Also make it dependent on presence of `missing` instead of parse error, which means that messages from complete commands that are immediately followed by parse errors are not filtered out anymore
4 lines
275 B
Text
4 lines
275 B
Text
weirdmacro.lean:1:6: error: expected no space before ':' or string literal
|
|
weirdmacro.lean:1:30-1:32: error: elaboration function for 'antiquot' has not been implemented
|
|
weirdmacro.lean:1:32: error: expected command
|
|
weirdmacro.lean:3:7-3:11: error: unknown identifier 'term'
|