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