Deactivate Gitlab CI.

[1uc]

Gitlab is currently completely broken and unusable. Hence we deactivate it until it can be used.

[pramodk]

@1uc: if it's matter of days (assuming its temporary gitlab glitch), is making it an optional from GitHub settings is an option as well?

[codecov-commenter]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 87.17%. Comparing base (39922a3) to head (1fbade8).

Additional details and impacted files

@@           Coverage Diff           @@
##           master    #1177   +/-   ##
=======================================
  Coverage   87.17%   87.17%           
=======================================
  Files         175      175           
  Lines       12878    12878           
=======================================
  Hits        11227    11227           
  Misses       1651     1651           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[1uc]

@pramodk it would still generate jobs on Gitlab. We don't know how they're gonna fix it. The "fix" might require us to cancel everything that didn't start. We can get it back with a simple git revert.

[1uc]

We had to disable the "Required" check, because not running is the same as not passing. We ended up disabling all "Required" checks, because we should merge when CI is green and not merge when it's red.

If CI is spuriously red, it needs to be fixed and if that's absolutely impossible disabled or removed.

[JCGoran]

LGTM, we should just remember to re-enable it when the cluster is fixed.