<div dir="ltr"><div>hi Javier</div><div><br></div><div>Its look good to me, please fill a pull request at Dave's repository.</div><div><br></div><div>Thanks</div><div>Walter<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Oct 8, 2019 at 2:41 PM Javier Candeira <<a href="mailto:javier@candeira.com">javier@candeira.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 8/10/19 14:17, Hong Yang wrote:<br>
<br>
>      > I think we need add this line to scons to make sure helpmap.scm<br>
>     presents, or<br>
>      > just have a default one in the repo. I'll check it later.<br>
<br>
<br>
It's done as an added commit in my current MR updating ubuntu18.04 install <br>
instructions. Please let me know if you want a separate MR, or anything <br>
handled differently.<br>
<br>
Cheers,<br>
J<br>
</blockquote></div>