Skip to content

Commit

Permalink
ensuring failing tests actually fail CI (#17)
Browse files Browse the repository at this point in the history
* ensuring failing tests actually fail CI

* fix bug
  • Loading branch information
kim-em authored Nov 14, 2023
1 parent 6ddd89a commit 0ddd89e
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 7 deletions.
6 changes: 3 additions & 3 deletions REPL/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -211,10 +211,10 @@ open REPL
/-- Get lines from stdin until a blank line is entered. -/
partial def getLines : IO String := do
let line ← (← IO.getStdin).getLine
return if line.trim.isEmpty then
line
if line.trim.isEmpty then
return line
else
line ++ (← getLines)
return line ++ (← getLines)

instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
toJson x := match x with
Expand Down
7 changes: 5 additions & 2 deletions test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,15 @@ for infile in $IN_DIR/*.in; do
# Compare the output with the expected output
if diff "$tmpfile" "$expectedfile"; then
echo "$base: PASSED"
# Remove the temporary file
rm "$tmpfile"
else
echo "$base: FAILED"
# Remove the temporary file
rm "$tmpfile"
exit 1
fi

# Remove the temporary file
rm "$tmpfile"
done

# Run the Mathlib tests
Expand Down
7 changes: 5 additions & 2 deletions test/Mathlib/test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,14 @@ for infile in $IN_DIR/*.in; do
# Compare the output with the expected output
if diff "$tmpfile" "$expectedfile"; then
echo "$base: PASSED"
# Remove the temporary file
rm "$tmpfile"
else
echo "$base: FAILED"
# Remove the temporary file
rm "$tmpfile"
exit 1
fi

# Remove the temporary file
rm "$tmpfile"
done

0 comments on commit 0ddd89e

Please sign in to comment.