The fun thing is that the files were not flagged by VirusTotal at the time of the release. In fact, the tor.exe
that was flagged in TorBrowser 12.5.6 is the exact same file, to the byte, as the one in 12.5.5, and nobody reported any issue when that release came out. (A few people mentioned downloading 12.5.5 as a workaround, but they were actually downloading the 32bit version, so it worked for them by accident).
That said, it’s not currently procedure to upload files to VirusTotal, and while it wouldn’t have helped with this specific incident, it’s still a good idea to do it. Ticket tor-browser-build#28175 tracks that, it was dormant for quite a while given there hasn’t been that kind of incident for some time, but I would expect some people to work on it in the future.