Add leading zeros to file name to keep them in order

[abe-101]

A neat little python script can add leading zero's to all the file names this way they will appear in order.
Something like this:

import sys,os,re

for file in sys.argv[1:]:
    if __file__ in file: continue
    number, name = file.split('-', 1)
    number = '{:0>4}'.format(number)
    new_name = f'{number}-{name}'
    os.rename(file,new_name)

PR #335 is the result of the above program.

[flonle]

It's worth noting that this is very closely related to #457. They should probably be part of the same proposal since they both require the website to be updated.

[mitchellirvin]

Thanks for the suggestion @abe-101 !

We'll include this as part of the work for #457. Closing out in favor of tracking there