Hi I am interested in how the git functionality works. How do you let the users deal with potential merge conflicts? How often do you commit and push? With every character that is typed or after the document is closed? Are branches used at all or do you stay on one main branch?