Draft: Check local git history before pushing a collection (#789)

Enrico Zinirequested to merge
task-git into task-pull-push

Missing:

  • user documentation
Edited by Enrico Zini

Merge request reports