diff --git a/default.nix b/default.nix index cff750254c..96305a7d32 100644 --- a/default.nix +++ b/default.nix @@ -101,7 +101,7 @@ rec { ''; postInstall = '' cp -r latex/ Makefile typecheck.time $out - sh checkTypeChecked.sh + sh checkTypeChecked.sh -m ''; extraExtensions = [ "hs" "cabal" "py" ]; }; diff --git a/src/checkTypeChecked.sh b/src/checkTypeChecked.sh index 43ceb2184d..d6681845a7 100755 --- a/src/checkTypeChecked.sh +++ b/src/checkTypeChecked.sh @@ -4,8 +4,10 @@ echo "Checking that all Agda files have been typechecked..." for agdaFn in $(find . -name '*.*agda'); do agdaiFn="_build/2.7.0/agda/${agdaFn%.*agda}.agdai" if [ "$(( $(stat -c "%Y" $agdaiFn) - $(stat -c "%Y" $agdaFn) ))" -lt "0" ]; then - echo " FAIL: $agdaiFn is not up-to-date" + if [ "$1" = "-m" ]; then + echo " FAIL: $agdaiFn does not exist. Please remove the corresponding agda file or import it somewhere, e.g. from the Everything module." + fi exit 1 fi done -echo " PASS: all Agda files have been typechecked" +echo " PASS: all Agda files have been typechecked."