aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index ba552ab302..4a6555a4f7 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1880,9 +1880,9 @@ function make_addon_quickchick {
# Flocq: Floating point library
function make_addon_flocq {
- if build_prep_overlay Flocq; then
+ if build_prep_overlay flocq; then
installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" ""
- logn autogen ./autogen.sh
+ log1 autoconf
logn configure ./configure
logn remake ./remake --jobs=$MAKE_THREADS
logn install ./remake install