After fixing bugs with duplicated sources for error traces (commit 5443dde) and coverage reports (bug #38), exactly the same sources file are excluded from each category. But at the same time, the may be duplicated source files across error trace and coverage reports and thus some small space are wasted.
In comparison with previous problems this one is much less important, since solving it will help to reduce overall reports size by just a few megabytes instated of tens of gigabytes.
Moreover, solving it will require a lot of changes in database schema, because currently coverage reports are optional and error trace source present only for unsafe results.
But this is still a small bug, which should be fixed some day.
After fixing bugs with duplicated sources for error traces (commit 5443dde) and coverage reports (bug #38), exactly the same sources file are excluded from each category. But at the same time, the may be duplicated source files across error trace and coverage reports and thus some small space are wasted.
In comparison with previous problems this one is much less important, since solving it will help to reduce overall reports size by just a few megabytes instated of tens of gigabytes. Moreover, solving it will require a lot of changes in database schema, because currently coverage reports are optional and error trace source present only for unsafe results. But this is still a small bug, which should be fixed some day.