[Agda-dev] google code is nearing the end

[Andrés Sicard-Ramírez]

On 25 March 2015 at 12:04, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> 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.

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...


-- 
Andrés