From df1c1cde12f25383ce528ec077dafb9ca5e1493a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 23 Jan 2022 02:55:16 +0100 Subject: [PATCH] refactor: make `LeanPaths` usage forward-compatible (leanprover/lake#48) --- Lake/Config/Workspace.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) }