From 71166020951ffc2c3b351ae9536e7249380aa509 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Wed, 26 May 2021 19:44:15 +0200
Subject: [PATCH] Inria CI "main" script: do not lower priority on macOS

I suspect "renice 10" has bad consequences on the Mac M1, so let's see
if removing it makes a difference.
---
 tools/ci/inria/main | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/ci/inria/main b/tools/ci/inria/main
index 4c133fa5997..5c38792267b 100755
--- a/tools/ci/inria/main
+++ b/tools/ci/inria/main
@@ -93,7 +93,7 @@ esac
 
 # be considerate towards other potential users of the test machine
 case "${OCAML_ARCH}" in
-  bsd|macos|linux) renice 10 $$ ;;
+  bsd|linux) renice 10 $$ ;;
 esac
 
 # be verbose and stop on error