aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/build
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-12-08 10:30:26 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-12-08 15:59:21 +0100
commitfb637d483d3637f0cf81eed92467f1ff491add2a (patch)
tree1b4867c4b00dde81009290145a89a97df6f841b9 /dev/build
parentd24aaa4d0e45dc3ec31c5f576516b01ded403dd8 (diff)
Fix paths in 32-bit windows build scripts.
Diffstat (limited to 'dev/build')
-rw-r--r--dev/build/windows/MakeCoq_86beta1_installer_32.bat4
-rw-r--r--dev/build/windows/MakeCoq_86rc1_installer_32.bat4
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