From 93447fd743c448f0d2b7eb3b59be6dec625bb7cf Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Thu, 1 Sep 2022 10:04:50 -0700 Subject: [PATCH] fix: run all tests so we can report how many tests failed --- lakefile.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 8f2d2cd..ea8d9a3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -59,6 +59,7 @@ different. -/ def execute (capture : Bool) : IO UInt32 := do let root : FilePath := "." / "test" let dirs ← walkDir root + let mut retVal : UInt32 := 0 for test in dirs do if test.extension = "lean" && test.fileName != "lakefile.lean" && !test.components.contains "lean_packages" then if let some fileName := test.fileName then @@ -76,8 +77,10 @@ def execute (capture : Bool) : IO UInt32 := do IO.println s!" SUCCESS" else IO.println s!" FAILED: diff {expected} {actual}" - return 1 - return 0 + retVal := retVal + 1 + if retVal > 0 then + IO.println s!"FAILED: {retVal} tests failed!" + return retVal script tests (args) do IO.println "Running diff tests for leanInk"