Closed mattulbrich closed 3 months ago
All modified and coverable lines are covered by tests :white_check_mark:
Project coverage is 37.85%. Comparing base (
fb58c33
) to head (bac61ee
).
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Can we get rid of the not semantically-correctly used todo items?
I find it very annoying if you look on a PR and Github says "5 out of 10 tasks done".
Can we get rid of the not semantically-correctly used todo items?
* [ ] Yes * [ ] No * [ ] Maybe?
I find it very annoying if you look on a PR and Github says "5 out of 10 tasks done".
Is this not exactly what the PR does?
I find it very annoying if you look on a PR and Github says "5 out of 10 tasks done".
That's the reason for the PR. If we have checkboxes than we should have them for things were 10/10 is the desired goal, and fewer should not be merged.
Intended Change
Updated and improved the pull request template.
Removing the checkboxes which always (if unticked) indicated that the PR is only partially finished in the overview. Replaced by item list from which items can be deleted.
Refining the structure. Adding a new subsection "Plan".
Type of pull request
Ensuring quality
n/a
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.