Commit 0a010579 authored by Ralf Jung's avatar Ralf Jung
Browse files

adjust regexp

parent 2b12b6fd
Pipeline #67785 passed with stage
in 4 minutes and 45 seconds
......@@ -6,5 +6,5 @@ s/subgoal/goal/g
/^File/d
# extra space removed in https://github.com/coq/coq/pull/16130
s/= $/=/
# coq/coq#16208 (this regex deletes an empty line followed by the "uses section variable" line)
/^$/{N;/.* uses section variable.*/d}
# delete "uses section variable" lines (https://github.com/coq/coq/pull/16208)
/^[^ ]+ uses section variables? .*\.$/d
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