Skip to content

Commit

Permalink
feat: also highlight executables
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Nov 21, 2024
1 parent 31cc4a8 commit 3537a46
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -116,10 +116,12 @@ library_facet examples lib : FilePath := do
moduleJobs.bindSync fun () trace => do
pure (hlDir, trace)


package_facet highlighted pkg : FilePath := do
let ws ← getWorkspace
let libs := pkg.leanLibs
let libJobs ← BuildJob.mixArray <| ← libs.mapM (fetch <| ·.facet `highlighted)
let exes := pkg.leanExes.map (·.toLeanLib)
let libJobs ← BuildJob.mixArray <| ← (libs ++ exes).mapM (fetch <| ·.facet `highlighted)
let buildDir := ws.root.buildDir
let hlDir := buildDir / "highlighted"
libJobs.bindSync fun () trace => do
Expand Down

0 comments on commit 3537a46

Please sign in to comment.