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

[Magnus Myreen]

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
>