[CakeML-Dev] [ExternalEmail] Re: readme_gen induced build failure at origin/master?

[Ramana Kumar]

Sorry, I missed Magnus's reply before I wrote mine. (And I missed a "not"
in mine.)

On 25 November 2016 at 16:03, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> If they're not in the repository, they are displayed nicely on the GitHub
> code browser.
>
> On 25 November 2016 at 15:51, <Michael.Norrish at data61.csiro.au> wrote:
>
>> 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.
>>
>> Michael
>>
>> On 25/11/16, 13:38, "Magnus Myreen" <magnus.myreen at gmail.com> wrote:
>>
>>     Hmm, I prefer to have a tool that is as strict as possible to keep up
>>     a high standard. Maybe it's OK to produce warnings for directories,
>>     but files should cause exit with an error. What do you think? --
>> Magnus
>>
>>     On 25 November 2016 at 12:57,  <Michael.Norrish at data61.csiro.au>
>> wrote:
>>     > This is probably an argument for letting readme_gen just issue a
>> warning and
>>     > ignore directories without readmeprefix files present.
>>     >
>>     >
>>     >
>>     > Michael
>>     >
>>     >
>>     >
>>     > From: "Michael.Norrish at data61.csiro.au" <
>> Michael.Norrish at data61.csiro.au>
>>     > Date: Friday, 25 November 2016 at 11:31
>>     > To: "developers at cakeml.org" <developers at cakeml.org>
>>     > Subject: [ExternalEmail] Re: [CakeML-Dev] readme_gen induced build
>> failure
>>     > at origin/master?
>>     >
>>     >
>>     >
>>     > Ah, I probably have stale directories from old commits and/or me
>> switching
>>     > to those old versions.
>>     >
>>     >
>>     >
>>     > Thanks,
>>     >
>>     > Michael
>>     >
>>     >
>>     >
>>     > From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>>     > Date: Friday, 25 November 2016 at 11:24
>>     > To: "Norrish, Michael (Data61, Canberra City)"
>>     > <Michael.Norrish at data61.csiro.au>
>>     > Cc: "developers at cakeml.org" <developers at cakeml.org>
>>     > Subject: Re: [CakeML-Dev] readme_gen induced build failure at
>> origin/master?
>>     >
>>     >
>>     >
>>     > Those directory names are rather suspicious: they look to be from
>> version1,
>>     > but the commit you mentioned is at the head of master (i.e.,
>> version 2).
>>     >
>>     > Is there something going on with environment variables, or are you
>> in the
>>     > wrong directory or something?
>>     >
>>     > On 25 November 2016 at 10:50, <Michael.Norrish at data61.csiro.au>
>> wrote:
>>     >
>>     > 7450870990a5254c72d19daf468141
>>     >
>>     >
>>     >
>>     >
>>     > _______________________________________________
>>     > Developers mailing list
>>     > Developers at cakeml.org
>>     > https://lists.cakeml.org/listinfo/developers
>>     >
>>
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161125/f036c9be/attachment.html>