[Agda-dev] google code is nearing the end
Andrés Sicard-Ramírez
asr at eafit.edu.co
Wed Mar 25 18:04:59 CET 2015
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
More information about the Agda-dev
mailing list