[Bug web/115391] Suggest add current size of git repository to git page

[redi at gcc dot gnu.org via Gcc-bugs]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=115391

--- Comment #1 from Jonathan Wakely <redi at gcc dot gnu.org> ---
You really shouldn't ever need to start again, you can just do:

git fetch origin && git reset --hard origin/master