3099633675
_gitUpdate() used to call 'git pull' then 'git checkout'. If the latter
command really did a branch switch, this could leave the local branch
behind its remote counterpart (that was hopefully fetched by the
'git pull'). From now on, we do:
git fetch origin
git checkout --force "$branch"
git pull --rebase
(the --force option was already there before in the form of -f). This
way, we can be sure that the local branch we check out is up-to-date
when the function returns.
Also replace short options by long ones for better readability of the
code, and use Bash's [[ ... ]] conditional construct instead of [ ... ]
for more efficiency---I think.
Note: 'git stash save' is documented as deprecated in favor of
'git stash push', however the latter appears to have been
introduced in 2017, therefore I believe it is too early to use it
in download_and_compile.sh.