Re: problem with git pull -r

[Jonas Hahnfeld]

Am Donnerstag, den 21.11.2019, 16:30 +0100 schrieb Werner LEMBERG:
> > Below is the console output.  Any ideas?
> 
> 
> Clone the repository anew, and everything should be fine again.

This works of course but is pretty destructive. A simple
 $ git fetch --prune
did the job for me. This removes branches under origin/ that don't
exist anymore on the server. In this case, it gets rid of
origin/dev/jmandereau which is now a directory (not sure if that is the
right term for git branches, but the corresponding (local)
.git/refs/remotes/origin/dev/jmandereau/ is now directory).

Regards,
Jonas

signature.asc
Description: This is a digitally signed message part