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