tree 5f26d367af63155c53327518f1c1d1554028bec2
parent 20c174860b77909bd5ad0f76db094e96ee787df8
author Jan Kundrát <jan.kundrat@cesnet.cz> 1586297308 +0200
committer Jan Kundrát <jan.kundrat@cesnet.cz> 1586309898 +0200

CI: start building with coverage profiling

This has to happen in two commits because the upcoming build job which
performs the comparison also builds the content of the repo from the
*previous* commit as-is. This means that this commit has to:

- enable `--coverage`,
- start generating that `coverage.xml`,
- teach artifact fetching code that the "-coverage-diff" suffix won't be
significant

Also remove one leftover which is no longer needed, really.

Change-Id: Ia8c73905f9f9eceb8347f8e83f402268d5cde1d0