Hi everybody,
we have tried to merge one of our feature-branches into our develop-branch and it failed. So far so bad. But now we are not able to merge anything to our develop-branch. The error says:
$ git push
Total 0 (delta 0), reused 0 (delta 0)
remote: error: cannot lock ref 'refs/heads/develop': Unable to create '/var/opt/gitlab/git-data-file09/repositories/madmen2017/madmen.git/./refs/heads/develop.lock': File exists.
remote:
remote: Another git process seems to be running in this repository, e.g.
remote: an editor opened by 'git commit'. Please make sure all processes
remote: are terminated then try again. If it still fails, a git process
remote: may have crashed in this repository earlier:
remote: remove the file manually to continue.
To https://gitlab.com/madmen2017/madmen.git
! [remote rejected] develop -> develop (failed to update ref)
error: failed to push some refs to 'https://gitlab.com/madmen2017/madmen.git'
Had anyone had this problem before? Has anyone a solution for this problem?
We are very grateful for every response 
Cheers
Rickib93 (MadMen)