diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-19 17:59:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-05 17:12:00 +0200 |
| commit | 843df88cd5b30d7c5ff744735baaea2c5a03a1c5 (patch) | |
| tree | 07f68a58da41769447b220be66ed5dc370c0d7fe /dev/build | |
| parent | 4e7d1a239fe325ca938db6144f77cdabd974ac17 (diff) | |
Print Coq build output.
Diffstat (limited to 'dev/build')
| -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 e17923951..45a5a5a4f 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 |