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

[Michael.Norrish at data61.csiro.au]

Ha.  Fair enough.

Michael

On 25/11/16, 15:58, "Magnus Myreen" <magnus.myreen at gmail.com> wrote:

    I checked them in so that they appear on github. I want them to be
    there so that one can see them while browsing the code on github. --
    Magnus
    
    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