On 13/05/12 21:39, Makarius wrote: > On Sun, 13 May 2012, Alfio Martini wrote: > >>> Alfio Martini at AlfioMartini-PC ~/Isabelle/PropTh/ISAR-PROP $ >>> ./makescript ### White space in ISABELLE_HOME may cause strange >>> problems! ### ISABELLE_HOME="/cygdrive/c/Users/Alfio >>> Martini/Desktop/Isabelle2012-RC2" > >>> make: /cygdrive/c/Users/Alfio: Command not found IsaMakefile:25: >>> recipe for target `/cygdrive/c/Users/Alfio' failed >> >> Somehow the command "isabelle make" here is not able to cope with >> the space in the string "Alfio Martini". > > The problem here is make, because it is inherently incapable of > working with spaces in file names. This is inherently not true. Make has many infelicities but this is not one of them. On Windows, you may also need to use the "call" command in order to get your command-lines to work. If you use appropriate escaping (backslashes in dependency and target lines; quoting in command lines), make will do the right thing. See the attached for an example. HOL4 on Windows has always coped with spaces in filenames and so can be installed in such 'awkward' places as C:\program files\HOL. Amusingly, HOL4 can't be installed in directories with spaces on Unix (at least under Moscow ML), because Moscow ML's shell scripts haven't been written with sufficient care. Dealing with spaces is a pain, but it's doable. Michael
foo\ bar: my\ dep echo "made something" > "$@" my\ dep: echo "this is a dependency" > "$@" .PHONY: clean clean: -@/bin/rm -f "my dep" "foo bar"
Description: OpenPGP digital signature