Source changes should include date of change

[Walter Bright]

On 9/8/2018 4:29 AM, Josphe Brigmo wrote:
> Um, I didn't say don't use Git!

I've done this manually before git. I can guarantee you that the dates put in 
the file are invariably wrong, incomplete, or non-existent.

But if you bring up a source file in github, and click on the "Blame" button, 
it'll tell you, for every line in the source, which PR last changed that line.