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.
-- 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.
