diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/hashmap/Makefile | 1 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Makefile | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/tests/fstar/hashmap/Makefile b/tests/fstar/hashmap/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/hashmap/Makefile +++ b/tests/fstar/hashmap/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/hashmap_on_disk/Makefile +++ b/tests/fstar/hashmap_on_disk/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) |