(with_ns): Remove dead code, since OPTION_DEFAULT_OFF means never unset.
commit6ba72723bbb8bfe644bb67137aa1b9483dbe9ee4
authorGlenn Morris <rgm@gnu.org>
Wed, 16 Jul 2008 08:09:53 +0000 (16 08:09 +0000)
committerGlenn Morris <rgm@gnu.org>
Wed, 16 Jul 2008 08:09:53 +0000 (16 08:09 +0000)
tree874ff868d202a08f7a690333dd614d6c2023b857
parent132d04752a194336e0ea965245294af64f27226f
(with_ns): Remove dead code, since OPTION_DEFAULT_OFF means never unset.
ChangeLog
configure.in