From fd470dab48c85d0229caceebadf1541a974530cd Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 20 Oct 2025 04:21:19 +0200 Subject: [PATCH] chore: tweak error message about weak options --- src/Lean/Language/Lean.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index ab3beca6cbe5..ab8d27d7e402 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -315,7 +315,7 @@ def reparseOptions (opts : Options) : IO Options := do | unless weak do throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}' -If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally" +If the option is defined in a library, use '-D{`weak ++ name}' to set it conditionally" let .ofString val := val | opts' := opts'.insert name val -- Already parsed