Hi,
We should all look at the old issues:
and move them to the new one:
instead of moving them automatically, we should take the chance to
clean up.
Please check, first for the issues that *you* added:
-> is it still relevant?
->if yes: add a new issue on GitHub
->close this issue, there is now an explicit “moved to GitHub” state.
Marcus