max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: make LeanPaths usage forward-compatible (leanprover/lake#48)

Browse source
This commit is contained in:
Sebastian Ullrich 2022-01-23 02:55:16 +01:00 • committed by GitHub
parent 6d7fc7216c
commit df1c1cde12
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Config/Workspace.lean
View file

@ -93,4 +93,4 @@ def leanSrcPath (self : Workspace) : SearchPath :=
/-- The `LeanPaths` of the workspace. -/
def leanPaths (self : Workspace) : LeanPaths :=
let pkgs := self.packageList
LeanPaths.mk (pkgs.map (·.oleanDir)) (pkgs.map (·.srcDir))
{ oleanPath := pkgs.map (·.oleanDir), srcPath := pkgs.map (·.srcDir) }