You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In Github, an issue is closed only when the PR is merged. This is even done automatically if your PR description contains Close #<issue number> so for instance Close #119 in #122.
The repair analysis takes too much time on real repos. To make progress, we can add an option to analyze the last nth commits.
The text was updated successfully, but these errors were encountered: