Marcus - do we just manually copy over the title and description (and any relevant comments) - or is there some tool to do this with?

Tim

On 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 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