diff options
Diffstat (limited to 'dev/build/windows/makecoq_mingw.sh')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d8cde39f8..ff67416b1 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1320,6 +1320,16 @@ function make_coq_installer { fi } +###################### ADDONS ##################### + + + +function make_addons { + for addon in $COQ_ADDONS; do + make_addon_$addon + done +} + ###################### TOP LEVEL BUILD ##################### make_sed @@ -1331,6 +1341,8 @@ list_files ocaml make_coq +make_addons + if [ "$INSTALLMAKE" == "Y" ] ; then make_mingw_make fi |