From 81cb2f6ca80811a22fbfeef1008e53fb6a8f514b Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 17 Jul 2021 13:27:33 -0400
Subject: [PATCH] refactor: use `modToFilePath` in `srcRoot` and `oleanRoot`

---
 Lake/Package.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Lake/Package.lean b/Lake/Package.lean
index 0f74ef1202..9a7fd46306 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -101,24 +101,24 @@ def depsDir (self : Package) : FilePath :=
 def srcDir (self : Package) : FilePath :=
   self.dir / self.config.srcDir
 
-def srcRoot (self : Package) : FilePath :=
-  self.srcDir / FilePath.withExtension self.moduleRootName "lean"
-
 def modToSrc (mod : Name) (self : Package) : FilePath :=
   Lean.modToFilePath self.srcDir mod "lean"
 
+def srcRoot (self : Package) : FilePath :=
+  self.modToSrc self.moduleRoot
+
 def oleanDir (self : Package) : FilePath :=
   self.dir / self.config.oleanDir
 
+def modToOlean (mod : Name) (self : Package) : FilePath :=
+  Lean.modToFilePath self.oleanDir mod "olean"
+
 def oleanRoot (self : Package) : FilePath :=
-  self.oleanDir / FilePath.withExtension self.moduleRootName "olean"
+  self.modToOlean self.moduleRoot
 
 def modToHashFile (mod : Name) (self : Package) : FilePath :=
   Lean.modToFilePath self.oleanDir mod "hash"
 
-def modToOlean (mod : Name) (self : Package) : FilePath :=
-  Lean.modToFilePath self.oleanDir mod "olean"
-
 def irDir (self : Package) : FilePath :=
   self.dir / self.config.irDir