From 77e72afe0a6338ae028e486db3bdc7b5477e8f88 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 20 Oct 2025 13:28:20 +1100
Subject: [PATCH] chore: tweak error message about weak options (#10844)

This PR tweaks the error message about options defined in libraries.
This was relevant for an option defined in Mathlib, but set in FLT.
---
 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 ab3beca6cb..ab8d27d7e4 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