Use OutputCheck pattern to avoid file paths variance in CI

dafny-lang · Feb 28, 2023 · 5164558 · 5164558
1 parent 060c997
commit 5164558
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/Test/wishlist/GoModule.dfy b/Test/wishlist/GoModule.dfy
@@ -1,6 +1,7 @@
 // RUN: %exits-with 3 %dafny /compile:3 /unicodeChar:0 /spillTargetCode:2 "%s" /compileTarget:go 2> "%t"
 // note: putting /compileTarget:go after "%s" overrides user-provided option
-// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: GoModuleConversions.go:10:3: imported and not used: "net/url"
 
 // This test used to work only because of a questionable Go-only feature
 // of mapping a Dafny string directly to a Go string when passed in or out of

diff --git a/Test/wishlist/GoModule.dfy.expect b/Test/wishlist/GoModule.dfy.expect