From 3a9ff92902df508074daa3017d1a71dae7e85248 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 21:08:35 +0100
Subject: Lean 4.25

---
 Common/String.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Common/String.lean')

diff --git a/Common/String.lean b/Common/String.lean
index 3edbd63..955affe 100644
--- a/Common/String.lean
+++ b/Common/String.lean
@@ -1,6 +1,6 @@
 namespace String
 
 def splitTrim (c : Char → Bool) (s : String) : List String :=
-  String.trim <$> s.split c
+  String.trim <$> s.splitToList c
 
 def notEmpty : String → Bool := not ∘ isEmpty
-- 
cgit v1.2.3