<div dir="ltr"><div dir="ltr">On Mon, Nov 4, 2019 at 4:52 PM Peter Wang <<a href="mailto:novalazy@gmail.com">novalazy@gmail.com</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Suggestions for a better name?<br></blockquote><div><br></div><div>I don't have any suggestions. The change is fine, so long as no one else can think of a better name.</div><div><br></div><div>Mark</div><div><br></div></div></div>