[Agda-dev] Migration of the issues from Google Code (Was: google code is nearing the end)

[Andrés Sicard-Ramírez]

Hi,

The current status is as follows:

1. Using the "Export to GitHub" bottom from

  https://code.google.com/export-to-github/export?project=agda

I migrated the issues to the repository

  https://github.com/asr/agda (*)

(After asking Google, I could use the "Export to GitHub" bottom
because Google temporarily raised the limit from 1000 issues to 2000
issues.)

2. What is next?

We need to "merge" the repository (*) into the Agda repository.

Because the "Export to GitHub" bottom doesn't allow

a) To migrate issues to a repository inside a GitHub organization

b) The repository created by the migration must have the same name as
the Google repository

and because after renaming a repository, GitHub

(see https://help.github.com/articles/renaming-a-repository/)

"In addition to redirecting web traffic, all git clone, git fetch, or
git push operations targeting the previous location will continue to
function as if made on the new location"

I don't know how to merge the repository (*) without deleting the Agda
repository.

I'll ask to GitHub about it.

Best,

-- 
Andrés