aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/MakeCoq_master_installer.bat (renamed from dev/build/windows/MakeCoq_trunk_installer.bat)2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/build/windows/MakeCoq_trunk_installer.bat b/dev/build/windows/MakeCoq_master_installer.bat
index f4f5827328..72640d5d79 100755
--- a/dev/build/windows/MakeCoq_trunk_installer.bat
+++ b/dev/build/windows/MakeCoq_master_installer.bat
@@ -16,7 +16,7 @@ call MakeCoq_SetRootPath
call MakeCoq_MinGW.bat ^
-arch=64 ^
-installer=Y ^
- -coqver=git-trunk ^
+ -coqver=git-master ^
-destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^
-destcoq="%ROOTPATH%\coq64_trunk_inst"