feat: Update style lint

This commit is contained in:
jstoobysmith 2025-03-21 11:22:23 -04:00
parent 08f0a01e9d
commit b56c689121
4 changed files with 4 additions and 4 deletions

View file

@ -30,7 +30,7 @@ body:
label: Scripts
description: Please check off these items as you complete them
options:
- label: Ensure `lake exe hepLean_style_lint` runs without errors.
- label: Ensure `lake exe style_lint` runs without errors.
- label: Ensure `lake exe TODO_to_yml mkFile` runs without errors.
- label: Ensure `lake exe stats mkHTML` runs without errors.
- label: Ensure `lake exe informal mkFile mkDot mkHTML` runs without errors.

View file

@ -45,8 +45,8 @@ name = "type_former_lint"
srcDir = "scripts"
[[lean_exe]]
name = "hepLean_style_lint"
srcDir = "scripts"
name = "style_lint"
srcDir = "scripts/MetaPrograms"
[[lean_exe]]
name = "find_TODOs"

View file

@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
def main (_: List String) : IO UInt32 := do
println! "Style lint ... "
let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]}
let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "style_lint"]}
println! styleLint.stdout
println! "Building ... "
let build ← IO.Process.output {cmd := "lake", args := #["build"]}