<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Mar 6, 2014 at 1:06 PM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">





<div lang="EN-GB" link="#0563C1" vlink="#954F72">
<div>
<p class="MsoNormal"><span style="font-size:12pt">What is this file?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12pt">nofib/real/HMMS/lib/haskell/Builtin.hi<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12pt">It’s a mystery!  Can we delete it?</span></p></div></div></blockquote><div><br></div><div><div>I think it's safe to assume that it was added by mistake. David even tried to remove it once:</div>

</div><div><br></div><div><div>tmp/ghc/nofib$ git log real/HMMS/lib/haskell/Builtin.hi</div><div>commit af36a39eed2e598c1f4c49dd726d3732b53b0f46</div><div>Author: David Terei <<a href="mailto:davidterei@gmail.com">davidterei@gmail.com</a>></div>

<div>Date:   Thu Jan 19 12:29:04 2012 -0800</div><div><br></div><div>    Revert "Move benchmarks into benchmark/ subdir."</div><div>    </div><div>    This reverts commit 0449cb065437fc8014b6669e5f1c2c8f4a926d16.</div>

<div>    </div><div>    Conflicts:</div><div>    </div><div>        .gitignore</div><div><br></div><div>commit 0449cb065437fc8014b6669e5f1c2c8f4a926d16</div><div>Author: David Terei <<a href="mailto:davidterei@gmail.com">davidterei@gmail.com</a>></div>

<div>Date:   Tue Jan 17 10:53:12 2012 -0800</div><div><br></div><div>    Move benchmarks into benchmark/ subdir.</div><div><br></div><div>commit 0bd88c95b14252969c9dd0a5eaa9da219af5f85f</div><div>Author: partain <unknown></div>

<div>Date:   Mon Jan 8 20:13:28 1996 +0000</div><div><br></div><div>    [project @ 1996-01-08 20:13:28 by partain]</div><div>    Initial revision</div></div><div><br></div></div></div></div>