From b48dfae100345376da25b17f3bace5e5e2cfa2f5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 24 Oct 2024 19:07:43 -0700 Subject: [PATCH] Hopeful compatibility with coq/coq#19599 Less blind editing for https://github.com/coq/coq/pull/19599#issuecomment-2422221331 --- examples/run-example-027.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/run-example-027.sh b/examples/run-example-027.sh index 34b35ea..072fbb0 100755 --- a/examples/run-example-027.sh +++ b/examples/run-example-027.sh @@ -87,17 +87,17 @@ find_bug "$EXAMPLE_INPUT" "$EXAMPLE_OUTPUT" -R . Foo || exit $? (\* File reduced by coq-bug-minimizer from original input, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines, then from [0-9]\+ lines to [0-9]\+ lines \*) (\* coqc version [^\*]*\*) \(Module Export Foo_DOT_A_WRAPPED\.\|Module Export Foo\.\) -Module Export A\. +Module \(Export \)\?A\. Definition foo : Type\. Admitted\. -\? + End A\. \(Module Export Foo\. Module A\. Include Foo_DOT_A_WRAPPED\.A\. End A\. -\)\? -\?Check Foo\.A\.foo : Set\. + +\)\?Check Foo\.A\.foo : Set\. EOF