]> git.pond.sub.org Git - empserver/commit
(set_option, delete_option): Gripe about unknown options. If multiple
authorMarkus Armbruster <armbru@pond.sub.org>
Thu, 11 Mar 2004 10:07:38 +0000 (10:07 +0000)
committerMarkus Armbruster <armbru@pond.sub.org>
Thu, 11 Mar 2004 10:07:38 +0000 (10:07 +0000)
commit71411189b448ad0408aa79a5b2d47a5ce6b4cd71
tree697e8e8a50683fcff76a4cae5904f562fb54c408
parent4caf8bb4408cbbabfb57cd4a3da9cd9c765d2f05
(set_option, delete_option): Gripe about unknown options.  If multiple
options have identical names in Options[], all but the first are
ignored.  This should never happen.
src/lib/gen/emp_config.c