diff options
| -rw-r--r-- | Makefile.in | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.in b/Makefile.in index c2c62a270..f14b9f5f0 100644 --- a/Makefile.in +++ b/Makefile.in @@ -82,6 +82,7 @@ endif GNATFLAGS=-gnat12 -gnaty3befhkmr -gnatwa -gnatwC -gnatf $(OPT_FLAGS) $(COVERAGE_FLAGS) $(ADA_FLAGS) GRT_FLAGS=$(OPT_FLAGS) $(COVERAGE_FLAGS) +GRT_ADAFLAGS:=$(ADA_FLAGS) ifeq "$(default_pic)" "true" GRT_FLAGS+=$(PIC_FLAGS) |