<!DOCTYPE html>
<html>
<head>
<title></title>
</head>
<body><div>Where did "make it long" come from? I'm not sure what the benefit is in using a long identifier.<br></div>
<div> </div>
<div>-Kevin Ballard</div>
<div> </div>
<div>On Mon, Feb 8, 2016, at 10:09 AM, Erica Sadun wrote:<br></div>
<blockquote type="cite"><div><p style="margin-top:0px;margin-bottom:16px;color:rgb(51, 51, 51);font-family:'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol';font-size:16px;background-color:rgb(255, 255, 255);">Several alternatives were put forward, of which <code style="font-family:Consolas, 'Liberation Mono', Menlo, Courier, monospace;font-size:14px;padding-top:0.2em;padding-right:0px;padding-bottom:0.2em;padding-left:0px;margin-top:0px;margin-right:0px;margin-bottom:0px;margin-left:0px;background-color:rgba(0, 0, 0, 0.0392157);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;">#setline</code> was the most popular. This failed the "make it specific and long" (and presumably avoid future naming conflicts) request. <br></p></div>
</blockquote><div> </div>
</body>
</html>