<div dir="ltr">If they're not in the repository, they are displayed nicely on the GitHub code browser.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 25 November 2016 at 15:51, <span dir="ltr"><<a href="mailto:Michael.Norrish@data61.csiro.au" target="_blank">Michael.Norrish@data61.csiro.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Next question: why are the README.md files checked in? As generated files that are easy to re-generate (contrast lem-generated files), I don’t think they should be in the repository.<br>
<span class="im HOEnZb"><br>
Michael<br>
<br>
On 25/11/16, 13:38, "Magnus Myreen" <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
<br>
</span><div class="HOEnZb"><div class="h5"> Hmm, I prefer to have a tool that is as strict as possible to keep up<br>
a high standard. Maybe it's OK to produce warnings for directories,<br>
but files should cause exit with an error. What do you think? -- Magnus<br>
<br>
On 25 November 2016 at 12:57, <<a href="mailto:Michael.Norrish@data61.csiro.au">Michael.Norrish@data61.csiro.<wbr>au</a>> wrote:<br>
> This is probably an argument for letting readme_gen just issue a warning and<br>
> ignore directories without readmeprefix files present.<br>
><br>
><br>
><br>
> Michael<br>
><br>
><br>
><br>
> From: "<a href="mailto:Michael.Norrish@data61.csiro.au">Michael.Norrish@data61.csiro.<wbr>au</a>" <<a href="mailto:Michael.Norrish@data61.csiro.au">Michael.Norrish@data61.csiro.<wbr>au</a>><br>
> Date: Friday, 25 November 2016 at 11:31<br>
> To: "<a href="mailto:developers@cakeml.org">developers@cakeml.org</a>" <<a href="mailto:developers@cakeml.org">developers@cakeml.org</a>><br>
> Subject: [ExternalEmail] Re: [CakeML-Dev] readme_gen induced build failure<br>
> at origin/master?<br>
><br>
><br>
><br>
> Ah, I probably have stale directories from old commits and/or me switching<br>
> to those old versions.<br>
><br>
><br>
><br>
> Thanks,<br>
><br>
> Michael<br>
><br>
><br>
><br>
> From: Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>><br>
> Date: Friday, 25 November 2016 at 11:24<br>
> To: "Norrish, Michael (Data61, Canberra City)"<br>
> <<a href="mailto:Michael.Norrish@data61.csiro.au">Michael.Norrish@data61.csiro.<wbr>au</a>><br>
> Cc: "<a href="mailto:developers@cakeml.org">developers@cakeml.org</a>" <<a href="mailto:developers@cakeml.org">developers@cakeml.org</a>><br>
> Subject: Re: [CakeML-Dev] readme_gen induced build failure at origin/master?<br>
><br>
><br>
><br>
> Those directory names are rather suspicious: they look to be from version1,<br>
> but the commit you mentioned is at the head of master (i.e., version 2).<br>
><br>
> Is there something going on with environment variables, or are you in the<br>
> wrong directory or something?<br>
><br>
> On 25 November 2016 at 10:50, <<a href="mailto:Michael.Norrish@data61.csiro.au">Michael.Norrish@data61.csiro.<wbr>au</a>> wrote:<br>
><br>
> 7450870990a5254c72d19daf468141<br>
><br>
><br>
><br>
><br>
> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
<br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</div></div></blockquote></div><br></div>