Skip to content

Commit 8cbbd0d

Browse files
committed
Improve the error message when a file hasn't been type checked
1 parent 6393a9e commit 8cbbd0d

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/checkTypeChecked.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ echo "Checking that all Agda files have been typechecked..."
44
for agdaFn in $(find . -name '*.*agda'); do
55
agdaiFn="_build/2.7.0/agda/${agdaFn%.*agda}.agdai"
66
if [ "$(( $(stat -c "%Y" $agdaiFn) - $(stat -c "%Y" $agdaFn) ))" -lt "0" ]; then
7-
echo " FAIL: $agdaiFn is not up-to-date"
7+
echo " FAIL: $agdaiFn does not exist. Please remove the corresponding agda file or import it somewhere."
88
exit 1
99
fi
1010
done
11-
echo " PASS: all Agda files have been typechecked"
11+
echo " PASS: all Agda files have been typechecked."

0 commit comments

Comments
 (0)