On 2016-10-10 16:13, Victor Shoup wrote:
One more question, relating to $(MAKE). There are a number of scripts besides the makefile that also invoke make. Should these also be modified? But then the mechanism would have to be different (environment variable?). Before I can sort that out, I would like to know what is the goal here? Is system make really not used in some environments? Or is there some magic in $(MAKE) within a makefile that is being used? If the latter, then I can probably just keep the other invocations of make are OK as is.
In other scripts, I think that "$MAKE" is mainly used to allow using a different version of make. For example, some systems might have a GNU make (installed as gmake) and a non-GNU make (installed as make). The MAKE environment variable can be set to the chosen make variant.
-- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
