Include Month in Formatting of Dates for RSS Feeds

Currently the date formatting in the RSS feed is wrong which can cause some aggregators to ignore that field. I have proposed a fix to this in #96.

However, the current feed still only publishes the year the article was published and not the month. I have written a small function to extract the month and year from the .tex file, but I am unsure where this would be implemented in the code as src/gen_json.py appears to be deprecated. Would it be possible to implement this somewhere so that the info.json file for each article includes the published month and year?

The following code makes some assumptions about the positioning of Shortheadings and jmlrheading which may not always be correct. The code in #96 code then be updated to check if the pubDate field is present in info.json and if not just use the year.

def getPubDate(src):
    # in v19 Shortheadings always follows jmlrheading heading so we split
    date = re.split(r"\\ShortHeadings", src)[0]
    # we then split by jmlrheading which leaves only that package input
    date = re.split(r"\\jmlrheading", date)[1]
    # we remove newlines to make it a one line string
    date = re.sub(r"\n", "", date)
    # extract a pattern of the form '{nn/nn}' or '{n/nn}' where n is a number
    # choose the last match to get pubDate and not submission date
    date = re.findall(r"\{\d?\d\/\d\d\}", date)[-1]
    # remove curly brackets
    date = re.sub(r"[{}]", "", date)
    return date

Start by tracing how article .tex files are converted into per-article info.json files; src/gen_json.py is identified as deprecated, so locate the current entry point. Compare the proposed getPubDate logic with the change discussed in #96, and consider the work complete when info.json includes the publication month and year for RSS consumption.