diff options
Diffstat (limited to 'util')
| -rw-r--r-- | util/pl/linux.pl | 2 | ||||
| -rw-r--r-- | util/pl/ultrix.pl | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/util/pl/linux.pl b/util/pl/linux.pl index 60ffc25930..fa281c8ba3 100644 --- a/util/pl/linux.pl +++ b/util/pl/linux.pl @@ -11,7 +11,7 @@ $rm='/bin/rm -f'; $cc='gcc'; if ($debug) - { $cflags="-g2 -ggdb -DREF_CHECK"; } + { $cflags="-g2 -ggdb -DREF_DEBUG"; } elsif ($profile) { $cflags="-pg -O3"; } else diff --git a/util/pl/ultrix.pl b/util/pl/ultrix.pl index c5e3be861c..1887794798 100644 --- a/util/pl/ultrix.pl +++ b/util/pl/ultrix.pl @@ -11,7 +11,7 @@ $rm='/bin/rm -f'; $cc='cc'; if ($debug) - { $cflags="-g -DREF_CHECK"; } + { $cflags="-g -DREF_DEBUG"; } else { $cflags="-O2"; } |