• Vincent Pelletier's avatar
    Stop using "git pull" and meaningless identity when updating. · 349522b6
    Vincent Pelletier authored
    We are never supposed to merge anything. We are supposed to just follow
    upstream. pull merges, so it's just the wrong tool.
    Instead, fetch and reset.
    It is not a problem to always reset, as user already cannot rely on
    repository's survival across updates: if there is any error reported by
    git command, the repository will be wiped out. So resetting will not do
    any more harm than what can already happen.
    Also, properly quote paths to protect against spaces (in both command and
    update-command).
    349522b6
software.cfg 1.69 KB