<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>