<div dir="ltr">That sounds cool. How does it keep track of which commit fixes which issue? Do you specify that when closing the issue?<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Mon, Dec 2, 2013 at 11:30 AM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Something that I would really like is being able to easily see the<br>
changes needed to fix various issues. In github, when a commit fixes<br>
an issue, the issue is automatically closed and a link to this commit<br>
is added to the issue tracker, so I can just click on it and see what<br>
was needed (so I can passively improve my understanding of the source<br>
code of Agda). Currently, I would need to "darcs pull" the latest<br>
version, figure out which change(s) fixed the issue, and figure out<br>
how to get the associated diff, so unless it’s something I’m really<br>
interested in I don’t usually do it.<br>
<br>
Guillaume<br>
<br>
2013/12/2 Jan Stolarek <<a href="mailto:jan.stolarek@p.lodz.pl">jan.stolarek@p.lodz.pl</a>>:<br>
<div class="HOEnZb"><div class="h5">>> I don't think there would be any huge advantages for us as main developers moving to github.<br>
> Just to be clear. I don't want to argue that github is the best place to host a project - I want<br>
> to argue that git is :-) Github has its flaws and for a large project it may not be suitable (as<br>
> is the case with GHC that only has github mirrors). I wouldn't mind having a git repo at<br>
> <a href="http://code.haskell.org" target="_blank">code.haskell.org</a>. This would allow me to have my own fork at github and at the same time pull new<br>
> changes from main repo. Still, I would not use Google Code for reporting bugs and send them to<br>
> the mailing list instead.<br>
><br>
> Janek<br>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>