From 9544a0572e318c0f16eeb7cf46665b38728e679c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 8 Aug 2022 04:17:25 -0700
Subject: [PATCH] fix: remove #check

---
 Lake/Config/Package.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 8b1f1c6809..540dfe83f9 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -206,8 +206,6 @@ structure Package where
   scripts : NameMap Script := {}
   deriving Inhabited
 
-#check String.dropRight
-
 hydrate_opaque_type OpaquePackage Package
 
 abbrev PackageSet := RBTree Package (·.config.name.quickCmp ·.config.name)