[Agda-dev] google code is nearing the end

Andrés Sicard-Ramírez asr at eafit.edu.co
Wed Apr 15 15:11:10 CEST 2015


On 14 April 2015 at 07:32, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> FYI, I didn't get the previous error when I press the "Export to
> GitHub" bottom, so it seems Google changed the maximum number of
> issues allowed to be exported. Testing...

After several failed attempts, I could migrate the issues to GitHub
(see https://github.com/asr/agda-complete-migration-test).

We lost the following information:

a) the attachments (the links don't work),
b) the milestones,
c) who created the issue and
d) who is assigned to the issue (this can be fixed issue by issue)

-- 
Andrés


More information about the Agda-dev mailing list