aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2018-05-14 16:29:01 +0200
committerMaxime Dénès2018-05-14 16:29:01 +0200
commit9af4d750c1e59ca8731790f7f620f413637dfc4d (patch)
tree5ea33fcf623832922fc2aee06fa262e4de10c949
parent63d63c95cd15cd932f100eda02653bdcb9e16e9e (diff)
parent22450b46cc0b9be39a7a365cde20c1c0abda0664 (diff)
Merge PR #7506: Add GitLab CI badge in first position.
-rw-r--r--README.md1
1 files changed, 1 insertions, 0 deletions
diff --git a/README.md b/README.md
index 883630acf1..4956da36db 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,6 @@
# Coq
+[![pipeline status](https://gitlab.com/coq/coq/badges/master/pipeline.svg)](https://gitlab.com/coq/coq/commits/master)
[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds)
[![Appveyor](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master)
[![Circle CI](https://circleci.com/gh/coq/coq/tree/master.svg?style=shield)](https://circleci.com/gh/coq/workflows/coq/tree/master)