From e7fe9f20ca0d8af8e8f5f5e8c512fd863c788827 Mon Sep 17 00:00:00 2001 From: Simon Marlow Date: Tue, 17 Oct 2006 13:22:15 +0000 Subject: [PATCH] compensate for gmp/configure sometimes not being executable --- rts/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rts/Makefile b/rts/Makefile index 9828f55..d187547 100644 --- a/rts/Makefile +++ b/rts/Makefile @@ -244,7 +244,7 @@ boot :: 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 -- 1.7.10.4