<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Jun 12, 2014 at 1:35 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Good!<br>
<br>
We should clarify how to work with the new repo in terms of branches etc.; draft a short note on the "best practices" on how to use or not use branching for<br>
<br>
* fixing a bug<br>
* adding a new feature<br>
<br>
Suggestions for a workflow model welcome!<br></blockquote><div><br></div><div>I'm not advocating for any particular approach as I'm not an agda developer, but I'll throw in my own bias and experience with git/github in general.</div>
<div><br></div><div>With github there is a very good reason to use a different branch for each bug fix. When you submit the pull request github tracks the branch you worked in but not the commit. The nice part is that it allows you to keep refining your pull request by committing to that branch. The downside is that if you work out of one branch (say master) then when you fix a bug, submit a pull request, and keep working, then all your commits will be included in the pull request whenever upstream gets around to looking at your PR.</div>
<div><br></div><div>Beyond that I personally don't like to introduce structured branching until there is a need (eg., someone says, "Hey, this is why we can't have nice things!"). Branches can be added lazily which gives a lot of flexibility in to this reactionary approach.</div>
<div><br></div><div>Your mileage my vary :)</div><div><br></div><div><br></div><div><br></div></div></div></div>