<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">2017-06-29 12:13 GMT+02:00 Augustin Trancart <span dir="ltr"><<a href="mailto:augustin.trancart@oslandia.com" target="_blank">augustin.trancart@oslandia.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Yes, agree with the idea of removing other big obsolete files as well.<br>
<br>
I'm not too worried about pull/pushes. If we require the files to be removed<br>
before merge, these commits would become unreachable after the force-push, and<br>
would eventually be garbage collected (providing we are careful at removing old<br>
branches).</blockquote><div><br></div><div>Not sure I understand that last paragraph.</div><div>My remark wrt rejecting pull requests (or pushes) with big files was to prevent this situation from happening again (in other words, as you said, "require the files to be removed before merge", but automate it).</div><div><br></div><div>Note also that GitHub will keep the files anyway in their special refs/pull/ references [1], you'll just never sync them (unless you want it) because (by default) Git only syncs refs/heads/ and refs/tags/</div><div>[1] <a href="https://help.github.com/articles/checking-out-pull-requests-locally/">https://help.github.com/articles/checking-out-pull-requests-locally/</a></div></div>
</div></div>