aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-25 11:26:33 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-05 17:12:00 +0200
commit802af9272442815012532818cffb6908ad5707e1 (patch)
treecb0b112d87d666b0ac3cc40b5228d7a853df8008 /dev
parentccf33e7aed7f6c8cdfa6ec6ebb6b5f094ed6989f (diff)
Get sources of cygwin packages after building the installer.
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/makecoq_mingw.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 5352b1dce..fd5f47d0f 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1272,7 +1272,7 @@ function get_cygwin_mingw_sources {
function make_coq_installer {
make_coq
make_mingw_make
- # get_cygwin_mingw_sources
+ get_cygwin_mingw_sources
# Prepare the file lists for the installer. We created to file list dumps of the target folder during the build:
# ocaml: ocaml + menhir + camlp5 + findlib