ci-wrapper: prevent piping from disabling automatic colors

Replace PR coq#18337

dev/ci/ci-wrapper.sh

@@ -14,7 +14,12 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 cd "${DIR}/../.." || exit 1
 
 export TIMED=1
-bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
+if [ -t 1 ] && command -v script > /dev/null; then
+  # prevent piping from disabling auto colors
+  script --quiet --flush --return -c "bash '${DIR}/${CI_SCRIPT}'" /dev/null 2>&1 | tee time-of-build.log
+else
+  bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
+fi
 code=$?
 echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log