diff options
| author | Nadrieril | 2024-04-18 11:26:51 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-04-18 11:27:08 +0200 |
| commit | 04f65cb173978ac9010ae88a24e6106382669fa1 (patch) | |
| tree | f9ca07a7e403e1d4003bcb393c964957c0bd7665 /Makefile | |
| parent | cfda3a990cb3b24d91ce5bf8d1ddec7b265beca5 (diff) | |
Address review comments
Diffstat (limited to '')
| -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 |