diff options
| -rw-r--r-- | Makefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.in b/Makefile.in index f14b9f5f0..bdd09dcc1 100644 --- a/Makefile.in +++ b/Makefile.in @@ -82,7 +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) +GRT_ADAFLAGS:=$(filter-out -gnata,$(ADA_FLAGS)) ifeq "$(default_pic)" "true" GRT_FLAGS+=$(PIC_FLAGS) |