diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index a9a5df6ffb..14a3bc7525 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -63,6 +63,8 @@ def buildUpdatedManifest (ws : Workspace) : LogIO Manifest := do return pkg else let depPkg ← loadDepPackage ws.dir result pkg.leanOpts dep.options + if depPkg.name ≠ dep.name then + logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'" modifyThe (NameMap Package) (·.insert dep.name depPkg) return depPkg return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}