Improve error message for option that is not defined and has now default value.

This commit is contained in:
Rob Vermaas 2013-06-28 21:34:33 +02:00
parent 9404b2cc12
commit 4278f778b4
1 changed files with 1 additions and 1 deletions

View File

@ -309,7 +309,7 @@ rec {
let opt = option.decl; in
opt.apply (
if isNotDefined then
opt.default or (throw "Not defined.")
opt.default or (throw "Option `${addName name}' not defined and does not have a default value.")
else opt.merge defs
)
);