Merge branch 'shared-runners' into 'master'

gitlab-ci: some build jobs are far too long on small instance runners, restore...

See merge request !530

.gitlab/build.yml

@@ -12,7 +12,7 @@
 
 .build_script_linux:
   extends: .build_script_common
-  tags: ['ci.inria.fr', 'linux']
+  tags: ['ci.inria.fr', 'linux', 'large']
   variables:
     GIT_CLONE_PATH: $CI_BUILDS_DIR/$CI_PROJECT_NAMESPACE/$CI_PROJECT_NAME
     SYSTEM: linux