Update file sizes on update

[waldoj]

The file sizes are hard-coded in the home page's HTML. But most of them change size each week. Ensure that the home page file listing reflects the reality of the file sizes.

[waldoj]

The best way to do this is probably to, at the time of updating the files, generate a JSON file of file names and sizes. Then, when the home page is loaded, use the JSON file (called server-side) to populate the list of file sizes.