Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

Commit

Permalink
fix: keyName regression caused by refactor
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed Jul 1, 2022
1 parent ab8098b commit 8c267a8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Lake/Build/Info.lean
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ inductive BuildInfo
/-! ### Build Key Helper Constructors -/

abbrev Module.facetBuildKey (facet : WfName) (self : Module) : BuildKey :=
.moduleFacet self.name facet
.moduleFacet self.keyName facet

abbrev Package.facetBuildKey (facet : WfName) (self : Package) : BuildKey :=
.packageFacet self.name facet
Expand Down

0 comments on commit 8c267a8

Please sign in to comment.