Files in tools/virtual

What was the original purpose of the files in ? Do we still need them? Is anyone still using them or planning to use them in the future? If not, can we remove them? @Gabor @tamas

My virus scanner will sometimes pick up this file (false positive): It’s not a big deal for me, but if it happens on my system, it may also happen for some users who clone the repo.

It was our CI system. We don’t need them any more.

For clarity, the files are now all removed in this commit.