diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 625771013a..f1d4aaf644 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -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) }