Verified Commit 06c4277c authored by Tej Chajed's avatar Tej Chajed
Browse files

Normalize focused goal output

Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.

std++ does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.
parent d8add3c1
Pipeline #55142 passed with stage
in 11 minutes and 22 seconds
# adjust for https://github.com/coq/coq/pull/13656 # adjust for https://github.com/coq/coq/pull/13656
s/subgoal/goal/g s/subgoal/goal/g
# merge with subsequent line for https://github.com/coq/coq/pull/14999
/[0-9]* focused goals\?$/{N;s/\n */ /;}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment