<div class="gmail_quote">2010/5/18 Baojian Hua <span dir="ltr"><<a href="mailto:huabj@mail.ustc.edu.cn">huabj@mail.ustc.edu.cn</a>></span><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I guess the reason is that the BUILDDATE<br>
info is automatically generated from the host, so it's highly<br>
platform dependent (and cause the error).<br></blockquote><div><br>This is a very good point. I've commited a change that hopefully forces 'date' to English.<br> <br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Btw: after some modification of the source, the self-compling<br>
succeeds, but the executable prints:<br>
<br>
"incorrect args from shell script"<br></blockquote><div><br>This one is puzzling. Could you edit /usr/bin/mlton and change the line 5 from<br>set -e<br>to <br>set -ex<br><br>Then run mlton again and copy-paste the result back to this list?<br>
</div></div>