chore: fix tests

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -148,9 +148,12 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
   let mut msgs ← result.failures.mapM (goalToMessageData · result.config)
   if result.config.verbose then
     let mut issues := result.issues
+    -- We did not find the following very useful in practice.
+    /-
     unless result.skipped.isEmpty do
       let m := m!"#{result.skipped.length} other goal(s) were not fully processed due to previous failures, threshold: `(failures := {result.config.failures})`"
       issues := .trace { cls := `issue } m #[] :: issues
+    -/
     unless issues.isEmpty do
       msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
     if let some msg ← mkGlobalDiag result.counters result.simp then

tests/lean/run/grind_pre.lean

@@ -161,8 +161,6 @@ right : r
     [prop] r
   [cases] Case analyses
     [cases] [1/2]: p = r
-[grind] Issues
-  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by

tests/lean/run/grind_split_issue.lean

@@ -25,8 +25,6 @@ h_1 : HEq ⋯ ⋯
     [eqc] {s, 0}
   [cases] Case analyses
     [cases] [1/2]: X c 0
-[grind] Issues
-  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/
 #guard_msgs (error) in
 example {c : Nat} (q : X c 0) : False := by