From 3537a46c54572d3a3a99a8bf7154d2f08990ee39 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 21 Nov 2024 15:57:53 +0100 Subject: [PATCH] feat: also highlight executables --- lakefile.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index 76f6987..c724fc1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -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