<div dir="ltr"><div><div>By mere curiosity, why didn&#39;t we follow the usual renaming process (and avoid losing the previous history in git) ?<br></div>It was just an upstream rename due to a trademark issue.<br><br></div>
H.<div class="gmail_extra"><br></div></div>