lake build Mathlib.Foo

Stream: lean4

[Kevin Buzzard]

I have managed to golf lake build +Mathlib.Data.Set.Lattice (the kind of thing I've been typing for the last few weeks) to lake build Mathlib.Data.Set.Lattice without the +. Does this do the same thing? It seems to...