Thanks, I ended up doing what you suggested. Should we document this git branch policy for contributors with commit access in the manual?
I think we should state it explicitly so there is no confusion for new contributors with commit access. all best, jgart
