<div dir="ltr">Hi all,<div><br></div><div style>With the Git move, the repository became "KRoC". Is there strong sentiment about this, or can I do a rename on the repository to "kroc," 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>