From c24fcbe937bcb84d7fd5e441ff6cbbad589fa096 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 May 2018 22:26:04 +0200
Subject: gitlab CI: remove math-classes job

It's redundant as a dependency of formal-topology.
---
 .gitlab-ci.yml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ac4304da13..2f5a000169 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -278,9 +278,6 @@ ci-iris-lambda-rust:
 ci-ltac2:
   <<: *ci-template
 
-ci-math-classes:
-  <<: *ci-template
-
 ci-math-comp:
   <<: *ci-template-flambda
 
-- 
cgit v1.2.3