come on

Rob23oba · Rob23oba · commit 23228b59cae2 · 2025-06-11T22:46:14.000+02:00
diff --git a/tests/lean/run/showTactic.lean b/tests/lean/run/showTactic.lean
@@ -127,7 +127,7 @@ error: 'show' tactic failed, no goals unify with the given pattern.
 
 In the first goal, the pattern
   x = 4
-is not definitionally equal to target
+is not definitionally equal to the target
   x = 1
 (Errors for other goals omitted)
 -/
