diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -101,8 +101,9 @@ test-all: test-no_nested_borrows test-paper \ .PHONY: clean-generated clean-generated: - # We can't put this line in `tests/Makefile` otherwise it will detect itself :D - grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | xargs rm + # 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 |