From ce724ed26b9326936c526ffd6ab0ab2266151913 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Apr 2026 01:03:01 +0000 Subject: [PATCH] chore: make Glob.ofString? public --- src/lake/Lake/Load/Toml.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 3056a8b999a7..271d8c427a3b 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -92,7 +92,7 @@ partial def takeName (ss : Substring.Raw) : (Substring.Raw × Name) := let (ss, n) := takeNamePart ss .anonymous if n.isAnonymous then (ss, .anonymous) else takeRest ss n -def Glob.ofString? (v : String) : Option Glob := do +public def Glob.ofString? (v : String) : Option Glob := do let (ss, n) := takeName v.toRawSubstring if n.isAnonymous then failure if h : ss.startPos.atEnd ss.str then