max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: remove #check

Browse source
This commit is contained in:
Mario Carneiro 2022-08-08 04:17:25 -07:00 • committed by tydeu
parent f40dbbcf02
commit 9544a0572e
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Config/Package.lean
View file

@ -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)