56d1b0 replace recommended git commands with working ones

Authored and Committed by Christian Boltz 3 years ago
    replace recommended git commands with working ones
    
    git fetch && git reset --hard   were recommended in #git because "git
    pull can cause trouble". So far for the theory.
    
    In practise, git fetch && git reset --hard  didn't update to the latest
    HEAD, leading to a trouble-free outdated version ;-)
    
    Switch over to git pull - even if it's not recommended, it works better
    ;-)