Fix option renaming
This commit is contained in:
parent
d5047faede
commit
44d6d88739
@ -159,7 +159,7 @@ rec {
|
|||||||
value = (opt.apply or id) merged;
|
value = (opt.apply or id) merged;
|
||||||
in opt //
|
in opt //
|
||||||
{ value = addErrorContext "while evaluating the option `${showOption loc}':" value;
|
{ value = addErrorContext "while evaluating the option `${showOption loc}':" value;
|
||||||
definitions = defsFinal;
|
definitions = map (def: def.value) defsFinal;
|
||||||
isDefined = defsFinal != [];
|
isDefined = defsFinal != [];
|
||||||
};
|
};
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user