.gitlab-ci.yml: enhance with mini-gmp builds

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8d44cbb739517a5006a26c00dede0d11dc5e7a46..eafe0d6c32909faae8ff1b8e75be8cdb063cd70a 100644 (file)
--- 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 &&