lake update just one dependency

Stream: lean4

[Joachim Breitner]

I’d like to update just one of my dependencies, but lake update seems to update all of them. I’d expect to be able to tell it to update just one or some … is that reasonable and just not implemented yet, or is that somehow not the right way to go about it?

[Joachim Breitner]

(currently, I do lake update, and then git checkout -p to undo the bumps I didn’t want)

[Mario Carneiro]

isn't that lean4#2405?

[Mario Carneiro]

oh it got rolled back

[Mario Carneiro]

oh wait no, it was just some extra syntax that was removed, lake update <pkg> was indeed added

[Joachim Breitner]

Ah, so I’m just a bit behind locally. Great, thanks!