> 1. Our commit history is not full of merges of tiny branches, which is > what GitHub (and I thought Gitlab) encourages.
Yes, that is right. But as I mentioned in a different thread, there are many projects where the maintainers agree to not use the merge button because of this. Since we are using gitlab we can actually go further than an agreement and disable the merge button entirely. > 2. Contributors can revise their patch series (by rewriting history of > that series), and committers can incorporate the final patch set, > rather than the whole sequence of iterations. This is what we > currently do; Gitlab should be able to recognize such patterns and > notice that the “merge request” can be closed, for instance. It depends on how much modification the maintainers make before pushing. It's git that has to recognize the commits as being the same. If a contributor can rebase his branch after the PR was merged without getting any conflicts, gitlab will also recognize that the PR was merged. Since it's a lot easier to iterate without spamming the mailing list we can in practice ask contributors to fix issues like indentation themselves, and if the worst case happens, PR can be closed manually (in the web interface). > 3. People (especially, ahem, me!) can work from the comfort of their > favorite editor/terminal, or at least without having to run lots of > JS code and clicking around all day long. That's what we all want. The only time it's required to use the web interface is when creating a new issue or a new PR. After that you can reply via email, rebase and push via git. > I haven’t used Gitlab so I don’t know whether these requirements are > satisfied. If you set up an instance of Gitlab-free-software-edition > and we do not have these problems, I’m happy! :-) Some adjustments to the workflow might have to be made, but I think we have to give it a test run of at least a week or two before throwing the towel ;-) Who wants to take on this? Any volunteers?