diff options
Diffstat (limited to 'win32/configure.bat')
| -rwxr-xr-x | win32/configure.bat | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/win32/configure.bat b/win32/configure.bat index a3df0bb4eb..7253ade28b 100755 --- a/win32/configure.bat +++ b/win32/configure.bat @@ -48,6 +48,7 @@ if "%1" == "--with-git" goto :git if "%1" == "--without-git" goto :nogit
if "%1" == "--without-ext" goto :witharg
if "%1" == "--without-extensions" goto :witharg
+if "%1" == "--with-gmp" goto :gmp
if "%opt:~0,10%" == "--without-" goto :withoutarg
if "%opt:~0,7%" == "--with-" goto :witharg
if "%1" == "-h" goto :help
@@ -210,6 +211,12 @@ goto :loop ; echo>>confargs.tmp %1 \
shift
goto :loop ;
+:gmp
+ echo>> ~tmp~.mak "WITH_GMP=yes" \
+ echo>>confargs.tmp %1=1 \
+ shift
+ shift
+goto :loop ;
:witharg
echo>>confargs.tmp %1=%2\
set witharg=1
|