summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-08-01 08:09:41 +0100
committerGitHub <noreply@github.com>2022-08-01 09:09:41 +0200
commit9653e0d6b092b5147aa1a7c4518dd747092e21b8 (patch)
treee84aafe7fa7fc6f4da63a07038f9d22729f6234e /tools
parenta225f3bd86cdbbbf666bae856d04e0eea1086398 (diff)
downloadocaml-9653e0d6b092b5147aa1a7c4518dd747092e21b8.tar.gz
Test 32-bit build in GitHub Actions (#11143)
* Add an i386 test to GitHub Actions * Correct the actions build script
Diffstat (limited to 'tools')
-rwxr-xr-xtools/ci/actions/runner.sh8
1 files changed, 2 insertions, 6 deletions
diff --git a/tools/ci/actions/runner.sh b/tools/ci/actions/runner.sh
index ede27f710a..de10bd1fd3 100755
--- a/tools/ci/actions/runner.sh
+++ b/tools/ci/actions/runner.sh
@@ -45,11 +45,7 @@ EOF
./configure $configure_flags
;;
i386)
- ./configure --build=x86_64-pc-linux-gnu --host=i386-linux \
- CC='gcc -m32 -march=x86-64' \
- AS='as --32' \
- ASPP='gcc -m32 -march=x86-64 -c' \
- PARTIALLD='ld -r -melf_i386' \
+ ./configure --build=x86_64-pc-linux-gnu --host=i386-pc-linux-gnu \
$configure_flags
;;
*)
@@ -60,7 +56,7 @@ EOF
}
Build () {
- $MAKE world.opt
+ $MAKE
echo Ensuring that all names are prefixed in the runtime
./tools/check-symbol-names runtime/*.a otherlibs/*/lib*.a
}