From df2a3679581f4dd054fa66cf0dbc97e754d5da81 Mon Sep 17 00:00:00 2001
From: Christian Krause <86738237+Bergschaf@users.noreply.github.com>
Date: Thu, 21 May 2026 12:17:58 +0200
Subject: [PATCH] doc: fix wrong example for String.split (#13787)

This PR fixes a small docsting error for `String.split`.
---
 src/Init/Data/String/Search.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/String/Search.lean b/src/Init/Data/String/Search.lean
index db44b4d3f4..a7675ad98e 100644
--- a/src/Init/Data/String/Search.lean
+++ b/src/Init/Data/String/Search.lean
@@ -251,7 +251,7 @@ Examples:
  * {lean}`("coffee tea water".split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
  * {lean}`("coffee tea water".split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
  * {lean}`("coffee tea water".split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
- * {lean}`("ababababa".split "aba").toList == ["coffee".toSlice, "water".toSlice]`
+ * {lean}`("ababababa".split "aba").toList == ["".toSlice, "b".toSlice, "ba".toSlice]`
  * {lean}`("baaab".split "aa").toList == ["b".toSlice, "ab".toSlice]`
 -/
 @[inline]