Skip to content
This repository was archived by the owner on Aug 24, 2024. It is now read-only.

Commit 4e2f41d

Browse files
committed
fix: remove debug output from tests
1 parent 1e61dc9 commit 4e2f41d

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

test/test.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,10 +43,10 @@ run_leanink () {
4343
# If the folder in which the file resides contains a lakefile we will use it to resolve any dependencies for the file
4444
if [[ -f "$directory/lakefile.lean" ]]; then
4545
echo "Running LeanInk with lakefile.lean - $file"
46-
(cd $directory && $LEANINK analyze $filename --lake lakefile.lean --verbose) || error "LeanInk failed - $file"
46+
(cd $directory && $LEANINK analyze $filename --lake lakefile.lean) || error "LeanInk failed - $file"
4747
else
4848
echo "Running LeanInk - $file"
49-
(cd $directory && $LEANINK analyze $filename --verbose) || error "LeanInk failed - $file"
49+
(cd $directory && $LEANINK analyze $filename) || error "LeanInk failed - $file"
5050
fi
5151
}
5252

0 commit comments

Comments
 (0)