Skip to content

Commit

Permalink
fix: compatibility with nightlies
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Jan 28, 2025
1 parent 73ee362 commit 63d1a95
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
1 change: 1 addition & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ jobs:
- "4.16.0-rc2"
- "nightly-2025-01-05"
- "nightly-2025-01-19"
- "nightly-2025-01-28"
platform:
- os: ubuntu-latest
installer: |
Expand Down
5 changes: 2 additions & 3 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -159,17 +159,16 @@ else

library_facet highlighted lib : FilePath := do
let ws ← getWorkspace
let mods ← lib.modules.fetch
let mods ← (← lib.modules.fetch).await
let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `highlighted)
let buildDir := ws.root.buildDir
let hlDir := buildDir / "highlighted"
moduleJobs.bindSync fun () trace => do
pure (hlDir, trace)


library_facet examples lib : FilePath := do
let ws ← getWorkspace
let mods ← lib.modules.fetch
let mods ← (← lib.modules.fetch).await
let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `examples)
let buildDir := ws.root.buildDir
let hlDir := buildDir / "examples"
Expand Down

0 comments on commit 63d1a95

Please sign in to comment.