Commit 97533618 by Barry Warsaw

Merge branch 'diffcov' into 'master'

Run diffcov for all merge requests

See merge request !251
2 parents 1aec5ff6 5d5dc3b6
Pipeline #6605695 for 97533618 passed in 42 minutes 11 seconds