From 2b12b6fd8bc789296868f9e953198a8ec32fc85f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 26 Jun 2022 23:19:20 -0400 Subject: [PATCH] normalize away new section variable info --- test-normalizer.sed | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test-normalizer.sed b/test-normalizer.sed index 3f9662bb..b9452d67 100644 --- a/test-normalizer.sed +++ b/test-normalizer.sed @@ -6,3 +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} -- GitLab