[Agda-dev] Migration of issues from Google Code

[Andrés Sicard-Ramírez]

Hi,

As it was mentioned by Ulf in other discussion, we should migrate our
issues from Google Code without weeks of manual labour.

>From what I've seen, our best option is to use Google's tools for this
job. Google only provides tools for migrating the issues to Bitbucket
(https://bitbucket.org/), GitHub or GitLab
(https://about.gitlab.com/).

I'll only report the non-common features between the above options.

Disadvantage of using the GitHub bug tracker:

* We cannot attach files

Disadvantages of using the Bitbucket or GitLab bug trackers:

* It is necessary to create an user in other site for reporting an issue.

* We cannot close issues using the commit messages.

Since we can use GitHub gists instead of attaching files when
reporting issues, I propose to migrate the issues to GitHub.

Any opinions?

P.S. The migration to GitHub requires some additional tests (e.g. we
cannot migrate the issues to a repository inside a GitHub
organization). Before continuing with these tests,  we need to chose
Agda's new bug tracker system.

Best,

-- 
Andrés