diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index e179239514..45a5a5a4f4 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1134,7 +1134,7 @@ function make_coq { if [[ $COQ_VERSION == 8.4* ]] ; then log1 make else - log1 make $MAKE_OPT + make $MAKE_OPT fi if [ "$INSTALLMODE" == "relocatable" ]; then |