[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