CI: Allow ci_build.sh to set a different C compiler.

diff --git a/build-aux/ci_build.sh b/build-aux/ci_build.sh
index 41cc2bc53b6d01111e3194e8347de19472e719e7..51b611a6c4bc688056e7b72471504f04dd799696 100755 (executable)
--- a/build-aux/ci_build.sh
+++ b/build-aux/ci_build.sh
@@ -23,6 +23,7 @@ USAGE="Usage: $0
   -d [encoders|decoders|bcj|delta|threads|shared|nls|small|ifunc|clmul|sandbox]
   -f [CFLAGS]
   -l [destdir]
+  -m [compiler]
   -n [ARTIFACTS_DIR_NAME]
   -p [all|build|test]
   -s [srcdir]"
@@ -55,7 +56,7 @@ ARTIFACTS_DIR_NAME="output"
 # Parse arguments #
 ###################
 
-while getopts a:b:c:d:l:n:s:p:f:h opt; do
+while getopts a:b:c:d:l:m:n:s:p:f:h opt; do
        # b option can have either value "autotools" OR "cmake"
        case ${opt} in
        h)
@@ -97,6 +98,10 @@ while getopts a:b:c:d:l:n:s:p:f:h opt; do
        ;;
        l) DEST_DIR="$OPTARG"
        ;;
+       m)
+               CC="$OPTARG"
+               export CC
+       ;;
        n) ARTIFACTS_DIR_NAME="$OPTARG"
        ;;
        s) SRC_DIR="$OPTARG"
@@ -237,6 +242,10 @@ then
 
                add_extra_option "$SMALL" "-DHAVE_SMALL=ON" ""
 
+               if test -n "$CC" ; then
+                       EXTRA_OPTIONS="$EXTRA_OPTIONS -DCMAKE_C_COMPILER=$CC"
+               fi
+
                # Remove old cache file to clear previous settings.
                rm -f "CMakeCache.txt"
                cmake "$SRC_DIR/CMakeLists.txt" -B "$DEST_DIR" $EXTRA_OPTIONS -DADDITIONAL_CHECK_TYPES="$CHECK_TYPE" -G "Unix Makefiles"