[Agda-dev] google code is nearing the end

[Andrés Sicard-Ramírez]

On 12 March 2015 at 13:48, Ulf Norell <ulf.norell at gmail.com> wrote:
> I played with a hack someone wrote in php or somesuch. I'm hoping that the
> official tools are a bit better....

Since it's not possible to use the Google tools in projects with more
than 1000 issues (see
https://code.google.com/p/support-tools/wiki/GitHubExporterFAQ#Are_all_projects_available_to_be_exported_to_GitHub_?),
we will need to use
https://code.google.com/p/support-tools/wiki/IssueExporterTool.

-- 
Andrés