On 9/7/05, <b class="gmail_sendername">Ross Paterson</b> &lt;<a href="mailto:ross@galois.com">ross@galois.com</a>&gt; wrote:<div><span class="gmail_quote"></span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
ross&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;2005/09/07 09:32:22 PDT<br><br>&nbsp;&nbsp;Modified files:<br>&nbsp;&nbsp;&nbsp;&nbsp;src/winhugs&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;winhugs.rc<br>&nbsp;&nbsp;Log:<br>&nbsp;&nbsp;from Neil Mitchell: remove unused resources.<br><br>&nbsp;&nbsp;(The files are retained in case someone finds a use for them.)
</blockquote><div><br>
I think it would be better to just get rid of them, especially if we
are going to write and maintain a gmake Makefile by hand. It is
confusing for somebody new to a project to understand why there are a
bunch of files that appear to never be used.<br>
<br>
- Brian<br>
</div><br></div><br>