b07384acbb
Initial options are now re-parsed and validated after importing. Cmdline option assignments prefixed with `weak.` are silently discarded if the option name without the prefix does not exist. Fixes #3403
9 lines
210 B
TOML
9 lines
210 B
TOML
name = "user_opt"
|
|
defaultTargets = ["UserOpt", "UserOptCmdline"]
|
|
|
|
[[lean_lib]]
|
|
name = "UserOpt"
|
|
|
|
[[lean_lib]]
|
|
name = "UserOptCmdline"
|
|
leanOptions = { myBoolOpt = true, weak.myNatOpt = 4, weak.notMyNatOpt = 5 }
|