aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMichael Soegtrop2020-07-04 19:50:28 +0200
committerMichael Soegtrop2020-07-04 19:50:28 +0200
commit6eecb3c9fc12317e3d753db54794244530991173 (patch)
treeee5fb396c7fcb3d81f18f8f236c0703cfeabaeda /dev
parent5facdb7fd256a5b3efe8c805f2666d613f302bd3 (diff)
Windows build: remove patch for windres architecture
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh4
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