compensate for gmp/configure sometimes not being executable

diff --git a/rts/Makefile b/rts/Makefile
index 9828f55..d187547 100644 (file)
--- a/rts/Makefile
+++ b/rts/Makefile
@@ -244,7 +244,7 @@ boot ::
        if [ -f gmp/config.status ]; then \
           cd gmp && CC=$(WhatGccIsCalled) ./config.status; \
         else \
        if [ -f gmp/config.status ]; then \
           cd gmp && CC=$(WhatGccIsCalled) ./config.status; \
         else \

-          cd gmp && CC=$(WhatGccIsCalled) ./configure --enable-shared=no \
+          cd gmp && CC=$(WhatGccIsCalled) $(SHELL) configure --enable-shared=no \

                        --host=`echo $(HOSTPLATFORM) | sed 's/i[567]86/i486/g'`; \
        fi
 
                        --host=`echo $(HOSTPLATFORM) | sed 's/i[567]86/i486/g'`; \
        fi