Run lake exe mk_all automatically

Stream: Polynomial Freiman-Ruzsa conjecture

[Rémy Degenne]

Small remark about that KL definition in PFR: I wanted to look at it but the LEAN link next to https://teorth.github.io/pfr/blueprint/sect0013.html#kl-div gives a 404

[Terence Tao]

Ah, I had put it in https://github.com/teorth/pfr/blob/master/PFR/kullback.lean but forgot to tell the main PFR.lean file about the existence of this file. Let me try to fix this now.

[Yaël Dillies]

(this seems to be a recurring problem that people forget to run lake exe mk_all. I will try to write some automation for this to happen automatically)

[Michael Rothgang]

How difficult is it to write a pre-push hook for this? (Granted, that's a more advanced feature, but perhaps that also goes some way.)

[Yaël Dillies]

I was planning to simply adapt the code in #12005, but feel free to investigate pre-push hooks! (I didn't even know they were a thing!)