From 97731353e81dba097c533a1b5be285508efc3384 Mon Sep 17 00:00:00 2001
From: Nikos Mavrogiannopoulos <nmav@redhat.com>
Date: Thu, 10 Mar 2016 17:45:07 +0100
Subject: [PATCH 3/3] .gitlab-ci.yml: enhance with mini-gmp builds

---
 .gitlab-ci.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8d44cbb..eafe0d6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -17,6 +17,14 @@ Build and Check (x86):
   - x86
   except:
   - tags
+Build and Check with mini-gmp:
+  script:
+  - ./.bootstrap &&
+    ./configure --disable-documentation --enable-mini-gmp && make -j4 &&
+    make check -j4
+  tags:
+  except:
+  - tags
 Build and Check with ubsan:
   script:
   - ./.bootstrap && 
-- 
2.5.0