On Thu, Feb 09, 2023 at 11:10:48PM +0100, Uwe Brauer wrote: [...] > Right now I am most worried about the situation in which the student > need to perform a merge. I regularly pull from their repos, check, write > my comments and push as soon as possible. Some day they want to push but > I have already pushed (the most standard situation in a server based > model, but, I have to see how well git pull [1] > will deal with this situation (I cross my finger that no conflicting > editing appears)
It's interesting that what you describe looks like the so-called "(merge/pull request review" I, for one, routinely do each day. Maybe you would be better off utilizing GitLab for this? Basically, you ask your students to push to their own branch and create what GitLab calls a "merge request" out the changes they have pushed. You then use the GitLab web interface to open so-called discussions which can be attached to specific ranges in the changes participaing in the MR. A student is then supposed to push a fix and and a comment to each discussion opened which can then either be continued or closed. It's not necessary to actually merge the MR if this is not needed: it can be closed and its branch deleted. GitLab makes opening MR's easy: when you push to a new branch, Git run by GitLab literally offers you a link to use to create an MR out what you've just pushed. But it can be done using specific actions from the GitLab UI. This way, there will literally be no possibility for races and no need to merge anything. GitLab will also send e-mail notifications both to the MR's author when you open/clone the discussions in it, and to you when someone comments on these discussions. [...] > [1] «fun fact»: «git pull» is in mercurial «hg fetch», while «git fetch» is in > mercurial «hg pull -u». Both system seem in many points being sort of > orthogonal to each other. Anyway that is a different story. Well, there's just a limited set of verbs to use for these actions, and I think what was ended up picked by each of the project is rather arbitrary. By the way, I'm in a camp which is opposed to ever touching pull in Git: to me, it has too much magic built in. I think it's better to use `git fetch` followed by explicit inspection of what are the differences of what you have locally and what you have fetched, followed by the conscious merge or rebase. A good testimony for this approach is given in [2]. [2] https://longair.net/blog/2009/04/16/git-fetch-and-merge/ -- You received this message because you are subscribed to the Google Groups "Git for human beings" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/git-users/20230210112917.mytitbgdppemojmb%40carbon.
