diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 15:01:47 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-05 17:12:00 +0200 |
commit | 8ac880bee5611a0a408158ff021277c6157eccce (patch) | |
tree | 161ec480c6a264534bc33a0ef9be87f61d870d88 /dev | |
parent | 843df88cd5b30d7c5ff744735baaea2c5a03a1c5 (diff) |
Print more of the Coq build output.
Diffstat (limited to 'dev')
-rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 45a5a5a4f..9507fe79b 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1119,11 +1119,11 @@ function make_coq { then if [ "$INSTALLMODE" == "relocatable" ]; then # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path - logn configure ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man + ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man elif [ "$INSTALLMODE" == "absolute" ]; then - logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" else - logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" + ./configure -debug -with-doc no -prefix "$PREFIXCOQ" fi # The windows resource compiler binary name is hard coded @@ -1138,13 +1138,13 @@ function make_coq { fi if [ "$INSTALLMODE" == "relocatable" ]; then - logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" fi - log2 make install - log1 copy_coq_dlls + make install + copy_coq_dlls if [ "$INSTALLOCAML" == "Y" ]; then - log1 copy_coq_objects + copy_coq_objects fi copq_coq_gtk |