<div dir="ltr">Hi all,<div><br></div><div style>With the Git move, the repository became &quot;KRoC&quot;. Is there strong sentiment about this, or can I do a rename on the repository to &quot;kroc,&quot; eliminating the mixed case?</div>
<div style><br></div><div style>It makes for a more difficult repository URL if we leave it mixed.</div><div style><br></div><div style>Cheers,</div><div style>M</div></div>