About the make variable... I can definitely see it's utility with make -j... I would guess that's the main advantage, and that's easy enough to fix in the makefile itself.
The other calls to make from other scripts are a bit more problematic. Would you say they are a priority? And if so, would one assume that a user would set the environment variable MAKE? As I understand it, in gnuc make, the variable MAKE is not an ordinary environment variable. It is a special variable with extra magic specific to make (including -j magic). -- 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.
