Re: [isabelle] "isabelle make" in windows-RC2



On 17/05/2012, at 22:57, Makarius <makarius at sketis.net> wrote:

> Google reveals some further slightly odd tricks for GNU Make:
> http://www.cmcrossroads.com/ask-mr-make/7859-gnu-make-meets-file-names-with-spaces-in-them

You'll need to check these all carefully yourself: this page's claim that you should use double backslashes does not work with the version of GNU make on my system.  Indeed, single backslashes do work. 

> This is again just some more motivation to get rid of make really soon
> now.
> 

I hope the brave new world will make it easy to generate files using things like mlyacc and mllex and to have the dependencies analysed and used in a make-like fashion.  Otherwise, you will just be off-loading  the use of make to users and the build system will be less useful.  If you are worried about different versions of make behaving differently, can't you just package make yourself (just as you do Java etc)?

Michael




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.