From eb30249b1118b5bea767354d5362f4afba97c82e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= <martin.dvorak@matfyz.cz>
Date: Tue, 21 Jan 2025 16:03:48 +0100
Subject: [PATCH] doc: make description of `pp.analyze` more precise (#6726)

As @nomeata told me, it should be "try to (...)" because even with
`pp.analyze` roundtripping often fails.
---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 0a2aed6e1a..5a1b7cb3c6 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -31,7 +31,7 @@ open Meta SubExpr
 register_builtin_option pp.analyze : Bool := {
   defValue := false
   group    := "pp.analyze"
-  descr    := "(pretty printer analyzer) determine annotations sufficient to ensure round-tripping"
+  descr    := "(pretty printer analyzer) try to determine annotations sufficient to ensure round-tripping"
 }
 
 register_builtin_option pp.analyze.checkInstances : Bool := {