Re: [GHC] #12223: Get rid of extra_files.py