Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #4553 from ThomasWaldmann/coverage-warning-1.1
get rid of confusing coverage warning, fixes #2069 (1.1-maint backport)
- Loading branch information