
<html>


<head>


<meta http-equiv="Content-Type" content="text/html; charset=utf-8">


</head>


<body text="#000000" bgcolor="#FFFFFF">


<div class="moz-cite-prefix">On 09/01/2020 16:11, Mehdi AMINI wrote:<br>


</div>


<blockquote type="cite" cite="mid:CANF-O=aQr0d-xcXjhDhx8rUS3RLow-O6r5u2vwrTViPwv2OZ_A@mail.gmail.com">


<br>


<div dir="ltr">


<div dir="ltr">


<div dir="ltr">


<div dir="ltr">


<div class="gmail_quote">


<blockquote class="gmail_quote" style="margin:0px 0px


                  0px


0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">


<div bgcolor="#FFFFFF">Please correct me if I'm wrong. I can repack for good measure, but I don't think it will affect anyone other than me.<br>


</div>


</blockquote>


<div><br>


</div>


<div>It seems that the way you processed the repo stayed fairly well packed right now, so there does not seem to be a need for anything here.</div>


<div>When I rewrote the MLIR history the impact of repacking was non negligible (~15% when comparing the size of the .git folder before/after repacking).</div>


</div>


</div>


</div>


</div>


</div>


</blockquote>


<p>After some time, I got a response back from GitHub. Apparently local packs are used during the upload, and GitHub do offer to repack if you ask them to do so.</p>


<p>So I agree with everything you said, and will make sure everything is repacked as well as possible before pushing -- when the time comes :)</p>


</body>


</html>