cat <<EOF >Makefile
noddy:
time echo 'WTF?'
EOF
make noddy TIME=time
make noddy
Compare results. With TIME=time, I see (emitted to stderr, I find) the
word time after the output from the command I wanted to time ...
without it, I see the output from timing the echo (like I intended). If
passing TIME=time seems bizarre, bear in mind that my (much larger)
Makefile used $(TIME) where the illustrative one uses time - I wanted to
have the option of timing a command, by setting TIME=time, or of just
running the command without timing it.
Now, man time says that time pays close attention to the TIME
environment variable, but passing TIME=time on make's command line (to
the *right* of make) shouldn't put it into the environment (should it ?)
I don't see any evidence (in the info pages - e.g. Name Index) for make
treating the name TIME specially.
Workaround: use the name TIMER rather than the name TIME for the
variable which is to be either unset (just run the command, don't time
it) or set to time when I want to time the command.
Eddy.
--
make --version
GNU Make version 3.77, by Richard Stallman and Roland McGrath.
Copyright (C) 1988, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98
Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.
