diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 38fd868b00..f9a225b9b6 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -103,9 +103,11 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
 @[builtin_term_elab Lean.Parser.Term.omission] def elabOmission : TermElab := fun stx expectedType? => do
   logWarning m!"\
     The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. \
-    It logs this warning and then elaborates like `_`.\
-    \n\nThe presence of `⋯` in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
-    These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
+    It logs this warning and then elaborates like '_'.\
+    \n\n\
+    The presence of '⋯' in pretty printing output is controlled by the 'pp.maxSteps', 'pp.deepTerms' and 'pp.proofs' options. \
+    These options can be further adjusted using 'pp.deepTerms.threshold' and 'pp.proofs.threshold'. \
+    If this '⋯' was copied from the Infoview, the hover there for the original '⋯' explains which of these options led to the omission."
   elabHole stx expectedType?
 
 @[builtin_term_elab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do
diff --git a/tests/lean/ppDeepTerms.lean.expected.out b/tests/lean/ppDeepTerms.lean.expected.out
index 3bc3c796bf..8b86c94c57 100644
--- a/tests/lean/ppDeepTerms.lean.expected.out
+++ b/tests/lean/ppDeepTerms.lean.expected.out
@@ -3,7 +3,7 @@ Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ : Nat
 ⋯.succ.succ.succ.succ.succ.succ.succ.succ.succ : Nat
 [1, 2, 3, 4, 5, 6, 7, 8] : List Nat
 [1, 2, 3, 4, 5, 6, 7, 8, ⋯] : List Nat
-ppDeepTerms.lean:39:32-39:33: warning: The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. It logs this warning and then elaborates like `_`.
+ppDeepTerms.lean:39:32-39:33: warning: The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. It logs this warning and then elaborates like '_'.
 
-The presence of `⋯` in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.
+The presence of '⋯' in pretty printing output is controlled by the 'pp.maxSteps', 'pp.deepTerms' and 'pp.proofs' options. These options can be further adjusted using 'pp.deepTerms.threshold' and 'pp.proofs.threshold'. If this '⋯' was copied from the Infoview, the hover there for the original '⋯' explains which of these options led to the omission.
 [1, 2, 3, 4, 5, 6, 7, 8, ?m] : List Nat