diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-12-08 10:30:26 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-12-08 15:59:21 +0100 |
commit | fb637d483d3637f0cf81eed92467f1ff491add2a (patch) | |
tree | 1b4867c4b00dde81009290145a89a97df6f841b9 /dev | |
parent | d24aaa4d0e45dc3ec31c5f576516b01ded403dd8 (diff) |
Fix paths in 32-bit windows build scripts.
Diffstat (limited to 'dev')
-rw-r--r-- | dev/build/windows/MakeCoq_86beta1_installer_32.bat | 4 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86rc1_installer_32.bat | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat index ff83087e7..f53232b65 100644 --- a/dev/build/windows/MakeCoq_86beta1_installer_32.bat +++ b/dev/build/windows/MakeCoq_86beta1_installer_32.bat @@ -4,5 +4,5 @@ call MakeCoq_MinGW.bat ^ -arch=32 ^
-installer=Y ^
-coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq64_86beta1_inst
+ -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat index 50672a6b5..96f43e16a 100644 --- a/dev/build/windows/MakeCoq_86rc1_installer_32.bat +++ b/dev/build/windows/MakeCoq_86rc1_installer_32.bat @@ -4,5 +4,5 @@ call MakeCoq_MinGW.bat ^ -arch=32 ^
-installer=Y ^
-coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq64_86rc1_inst
+ -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86rc1_inst
|