From ffd5bc0f6931f5d0afe6e66bfa327aedf6753f6e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 18 Oct 2021 18:01:31 -0400
Subject: [PATCH] refactor: narrow Lean imports

---
 Lake/Attributes.lean | 2 +-
 Lake/LeanConfig.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lake/Attributes.lean b/Lake/Attributes.lean
index 3d59d3fe5e..d9fac00590 100644
--- a/Lake/Attributes.lean
+++ b/Lake/Attributes.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean
+import Lean.Attributes
 
 open Lean
 namespace Lake
diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean
index 67a72f8503..b7dbd97d1a 100644
--- a/Lake/LeanConfig.lean
+++ b/Lake/LeanConfig.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean
+import Lean.Elab.Frontend
 import Lake.Package
 import Lake.Attributes