Update TODO_to_yml.lean
This commit is contained in:
parent
57c7b5a8f0
commit
be13241fe5
1 changed files with 2 additions and 1 deletions
|
@ -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
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue