diff options
Diffstat (limited to 'src/ortho/debug/Makefile')
| -rw-r--r-- | src/ortho/debug/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ortho/debug/Makefile b/src/ortho/debug/Makefile index 3e8bb5913..1dd2d0f06 100644 --- a/src/ortho/debug/Makefile +++ b/src/ortho/debug/Makefile @@ -24,7 +24,7 @@ GNATMAKE=gnatmake CC=gcc CFLAGS=-g ALL_GNAT_FLAGS=-pipe -g -gnato -gnatwaeu -gnatf -gnaty3befhkmr -GNATMAKE_FLAGS=-m $(ALL_GNAT_FLAGS) $(GNAT_FLAGS) -aI$(ortho_srcdir) -aI$(orthobe_srcdir) -aI. +GNATMAKE_FLAGS=-m $(ALL_GNAT_FLAGS) $(GNATFLAGS) -aI$(ortho_srcdir) -aI$(orthobe_srcdir) -aI. #LARGS=-largs -static SED=sed |