-
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