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