lake exe cache ge

Stream: lean4

[Kevin Buzzard]

I just failed to type "lake exe cache get" properly; I wrote lake exe cache ge. But lake is now working away doing stuff and I'm too scared to interrupt it (downloading a new version of Lean). My instinct here is to be surprised that a malformed command still makes lake do some work before announcing that I'd written something nonsensical. Is this behaviour OK or unexpected?

[Ruben Van de Velde]

I think it's compiling the cache command, and only when it's done that, it can check the further arguments

[Ruben Van de Velde]

Should be done soon