From 87947ba45b3aa5121b7376785b3844443128822c Mon Sep 17 00:00:00 2001
From: Alok Singh <8325708+alok@users.noreply.github.com>
Date: Sun, 28 Apr 2024 02:44:55 -0700
Subject: [PATCH] fix: coe string -> name removed, explicitly call
 String.toName

The coercion was removed recently, and it's backwards compatible.
---
 lakefile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 95c963b..a421964 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -106,7 +106,7 @@ lean_exe download {
 
 
 lean_lib LeanCopilotTests {
-  globs := #[.submodules "LeanCopilotTests"]
+  globs := #[.submodules "LeanCopilotTests".toName]
 }