On 18 Mar 2019, at 19:26, Tim Mackinnon <tim@testit.works> wrote:Marcus - do we just manually copy over the title and description (and any relevant comments) - or is there some tool to do this with?TimOn 18 Mar 2019, at 07:38, Marcus Denker <marcus.denker@inria.fr> wrote: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 toclean 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