- ( set -e; \
- cd $i ; \
- echo '' ; \
- echo "*** configuring $i ..." ; \
- make -f Makefile.BOOT BOOT_DEFINES="-P $i $setup -C mkworld -DTopDirPwd=$hardtop"; \
- echo '' ; \
- echo "*** making Makefiles in $i ..." ; \
- make Makefile ; \
- make Makefiles \
+ ( set -e; \
+ cd $i ; \
+ echo '' ; \
+ echo "*** configuring $i ..." ; \
+ @MakeCmd@ -f Makefile.BOOT BOOT_DEFINES="-P $i $setup -C mkworld -DTopDirPwd=$hardtop"; \
+ echo '' ; \
+ echo "*** making Makefiles in $i ..." ; \
+ @MakeCmd@ Makefile ; \
+ @MakeCmd@ Makefiles \