From be13241fe5bb0812bd34791cc28987c9ae6ca8e6 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 3 Feb 2025 06:40:27 +0000
Subject: [PATCH] Update TODO_to_yml.lean

---
 scripts/MetaPrograms/TODO_to_yml.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/scripts/MetaPrograms/TODO_to_yml.lean b/scripts/MetaPrograms/TODO_to_yml.lean
index 5fa6fb1..09692ad 100644
--- a/scripts/MetaPrograms/TODO_to_yml.lean
+++ b/scripts/MetaPrograms/TODO_to_yml.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Basic
 import HepLean.Meta.TODO.Basic
+import Mathlib.Lean.CoreM
 /-!
 
 # Turning TODOs into YAML
@@ -23,7 +24,7 @@ def todoToYAML (todo : todoInfo) : MetaM String := do
   return s!"
 - content: \"{todo.content}\"
   file: {todo.fileName}
-  githubLink: {← Name.toGitHubLink todo.fileName todo.line}
+  githubLink: {Name.toGitHubLink todo.fileName todo.line}
   line: {todo.line}"
 
 unsafe def todosToYAML : MetaM String := do