diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 6ceb7f54b2..cc9fd13fdc 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1401,10 +1401,6 @@ function make_coq { logn configure ./configure -with-doc no -prefix "$PREFIXCOQ" fi - # The windows resource compiler binary name is hard coded - sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build - sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true - # 8.4x doesn't support parallel make if [[ $COQ_VERSION == 8.4* ]] ; then log1 make |