On 10 Oct 2017, at 17:49, Rainer Müller <[email protected]> wrote:
>  git reset --hard
>  git clean --force

That worked, but the question remains. Is there anything in port that could 
have messed the repo? Maybe an incomplete sync?

Reply via email to