From 06c4277c9c07f65454469b70c38f4fb2959a4493 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 13 Oct 2021 09:56:53 -0400
Subject: [PATCH] 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.
---
test-normalizer.sed | 2 ++
1 file changed, 2 insertions(+)
diff --git a/test-normalizer.sed b/test-normalizer.sed
index 97b8c63c..7a35762d 100644
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
@@ -1,2 +1,4 @@
# adjust for https://github.com/coq/coq/pull/13656
s/subgoal/goal/g
+# merge with subsequent line for https://github.com/coq/coq/pull/14999
+/[0-9]* focused goals\?$/{N;s/\n */ /;}
--
GitLab