[Agda-dev] Push your changes because the Agda repository will be deleted

[Andrés Sicard-Ramírez]

Hi,

The migration of the issues from Google Code to GitHub requires:

a) *Delete* the current Agda repository and

b) Create a new repository contains the issues migrated from Google Code

Please push your changes asap.

If you push anything (commits, branches, tags) please drop me a line.

Thanks,

-- 
Andrés