[Agda] Contributing: good first issues

[Herminie Pagel]

The contribute page of the user manual was updated with the information of
this thread:
https://agda.readthedocs.io/en/latest/contribute/index.html

Github has a standard label named "good first issues" for potential
first-time contributors that now is empty but could also be used:
https://github.com/agda/agda/labels/good%20first%20issue

-- h

Am Mi., 18. Dez. 2019 um 21:23 Uhr schrieb Marko Dimjašević <
marko at dimjasevic.net>:

> On Mon, 2019-12-16 at 12:34 +0100, Nils Anders Danielsson wrote:
> > On 2019-12-13 11:01, Ulf Norell wrote:
> > > There is a `difficulty: easy` label on GitHub (no guarantees that
> > > it's
> > > always accurate though).
> >
> > There is also "help wanted".
>
>
> Thank you!
>
>
> Kind regards,
> Marko Dimjašević
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191219/67070237/attachment.html>