<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Sebastian<br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">+  /*</div><div class=""><div class="">+   * Excessively long comments should be broken up at a word boundary or<br class="">+   * somewhere that makes sense, for example.<br class="">+   */<br class="">+<br class="">+Note that multiline comments have a single asterisk aligned with the asterisk<br class="">+in the opening ``/*``. </div></div></blockquote><div class=""><br class=""></div><br class=""><blockquote type="cite" class=""><div class=""><div class="">The closing ``*/`` should go at the end of the last line.<br class=""></div></div></blockquote><div class=""><br class=""></div><div class="">I think this is closer to what was discussed earlier:</div><div class=""><br class=""></div><div class="">The closing ``*/`` should appear on a line by itself at the end.</div></div><div><br class=""></div><div class=""><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">--------------------------------------------------------------------<br class="">Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204<br class="">Lero@TCD, Head of Software Foundations & Verification Research Group<br class="">School of Computer Science and Statistics,<br class="">Room G.39, O'Reilly Institute, Trinity College, University of Dublin<br class="">                         <a href="http://www.scss.tcd.ie/Andrew.Butterfield/" class="">http://www.scss.tcd.ie/Andrew.Butterfield/</a><br class="">--------------------------------------------------------------------</div>
</div>

<br class=""></body></html>