[Agda] github on Standard library

[Mateusz Kowalczyk]

On 23/01/14 11:31, Sergei Meshveliani wrote:
> I have reopened issue #2.
> 
> 1. I have closed it by mistake, because I do not find the button
> "submit" (a comment) and thought that "close" stands for "submit". 
> 
> 2. There have appeared several duplicated comments of mine to this
> issue, and I do not see how can I remove them, do not find the
> corresponding buttons.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

1. When you have the permission to close the issue (you're either the
repo collaborator or the issue creator), you should be given ‘Comment &
close’ and ‘Comment’ buttons. As you found out, ‘close’ one closes the
issue.

2. I don't remember if you can remove your comments. You can usually
edit them by clicking at the button at the corner of the comment. Not
sure what the requirement is there, you might only be able to do it on
your last post or something. Repository collaborator can remove the
extra comments for you.

-- 
Mateusz K.