diff options
Diffstat (limited to 'Makefile')
| -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: |