wanted prebuild release

Stream: general

[Kevin Buzzard]

~/lean-projects/mathlib4$ lake build +Mathlib.Algebra.Group.Opposite
info: downloading component 'lean'
177.5 MiB / 177.5 MiB (100 %)  28.5 MiB/s ETA:   0 s
info: installing component 'lean'
warning: wanted prebuilt release, but release repository and tag was not known
Building Std.Util.ExtendedBinder
Building Std.Lean.TagAttribute
Building Std.Tactic.HaveI
...

Apparently lake wanted a prebuilt release. Is this anything to worry about?

[Gabriel Ebner]

This should be fixed with https://github.com/JLimperg/aesop/pull/34