ci-build: be nice to other users and run at lower priority

2017-09-10 11:12:27 +02:00 · 2017-09-10 11:12:27 +02:00 · 0eb129e276
parent 76f5f62dda
commit 0eb129e276
1 changed files with 5 additions and 0 deletions
--- a/tools/ci-build
+++ b/tools/ci-build
@ -86,6 +86,11 @@ esac

 #########################################################################

+# be considerate towards other potential users of the test machine
+case "${OCAML_ARCH}" in
+  bsd|macos|linux) renice 10 $$ ;;
+esac
+
 # be verbose and stop on error
 set -ex