diff options
| author | Son HO | 2024-04-19 08:24:37 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-19 08:24:37 +0200 |
| commit | ad764b07c7a576eb509e08a29868e719fe5d8a84 (patch) | |
| tree | 678ae9c0edcf90925b5db65c8f2ada3d68073f9a /Makefile | |
| parent | caedb227fcf018a5e9e6f5627144a9bf0b5484c3 (diff) | |
| parent | 04f65cb173978ac9010ae88a24e6106382669fa1 (diff) | |
Merge pull request #132 from AeneasVerif/regen-tests
Ensure we regenerate files properly in CI
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 7 insertions, 1 deletions
@@ -83,7 +83,7 @@ doc: cd compiler && dune build @doc .PHONY: clean -clean: +clean: clean-generated cd compiler && dune clean # Test the project by translating test files to F* @@ -99,6 +99,12 @@ test-all: test-no_nested_borrows test-paper \ test-loops \ test-arrays test-traits test-bitwise test-demo +.PHONY: clean-generated +clean-generated: + # We can't put this line in `tests/Makefile` otherwise it will detect itself. + # FIXME: generation of hol4 files is deactivated so we don't delete those. + grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm + # Verify the F* files generated by the translation .PHONY: verify verify: |