Thanks, everybody.

I dared asking that question because I didn't want to miss any obvious solution

> Honestly, I would simply make a new branch, put my stuff there and leave it. I assume that your current local copy has been pulled and is recent.

I decided to go this way, and pushed a branch to gitlab.

Not only because it's already a difficult task under normal circumstances, but because the commit history is a big mess on our server.

Two colleagues did irregular big commits of all changed files (unfortunately including mine) with commit messages like "status" ,"new status", "last status".

Probably I could ditch those, but it would be a waste of time trying to discuss with them. It's already difficult enough to keep my own house clean.

Again thanks everybody! :)