diff options
Diffstat (limited to 'flake.nix')
| -rw-r--r-- | flake.nix | 9 |
1 files changed, 3 insertions, 6 deletions
@@ -75,23 +75,20 @@ export AENEAS_EXE=./aeneas # Copy the tests - mkdir tests-copy cp -r tests tests-copy - # TODO: remove the test files to make sure we regenerate exactly - # the files which are checked out (we have to be careful about - # files like lakefile.lean, and the user hand-written files) - # Run the tests with extra sanity checks enabled # Remark: we could remove the file + make clean-generated OPTIONS=-checks make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests # and the original tests - if [[ $(diff -rq tests tests-copy) ]]; then + if diff -rq tests tests-copy; then echo "Ok: the regenerated test files are the same as the checked out files" else echo "Error: the regenerated test files differ from the checked out files" + diff -ru tests tests-copy exit 1 fi ''; |