Now the "pull changes" button stays, while no automatic pull is executed, if it brings changes.
- User 1 creates doctypeU1-1 on master
- User 2 creates doctypeU2-1 on master
- User 1 navigate to 'document types' editor by clinking on the tree on on the left of the screen
- An icon indicating that something may be pulled has been shown
- a pop up asks for "save/discard/cancel" the modified (new) doctype
- click discard (or save)
- creates codtypeU1-2 on master
- "Your changes are commited and pushed" popup
- no more indicator of something to pull
Problem: the project has not been reloaded, and in the tree on the left, I do not see the doctypeU2-1, even if I see the commit adding it if I navigate to "Branch Management"
Refreshing the page solves the problem.