From df3449f44b4dcf12c6f39b14b8d280680ada533c Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 10 Jun 2020 13:08:50 +0100 Subject: [PATCH] Fix the other clashing test output I don't understand the difference here - there's probably a commit I hadn't merged earlier that affected the name generation. --- tests/idris2/coverage008/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index 77b301b2d9..76fe3b30a9 100644 --- a/tests/idris2/coverage008/expected +++ b/tests/idris2/coverage008/expected @@ -1,6 +1,6 @@ 1/1: Building wcov (wcov.idr) Main> Main.tfoo is total Main> Main.wfoo is total -Main> Main.wbar is not covering due to call to function Main.with block in 1376 +Main> Main.wbar is not covering due to call to function Main.with block in 1372 Main> Main.wbar1 is total Main> Bye for now!