From 4567e3a0a44a6c398375effa7d9a49342172512a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 24 Feb 2017 02:28:27 +0100
Subject: [travis] [External CI] fiat-parsers

---
 .travis.yml               |  1 +
 Makefile.ci               |  2 +-
 dev/ci/ci-fiat-parsers.sh | 12 ++++++++++++
 3 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100755 dev/ci/ci-fiat-parsers.sh

diff --git a/.travis.yml b/.travis.yml
index de16f2d0b4..5ed0809a52 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -30,6 +30,7 @@ env:
   - TEST_TARGET="ci-cpdt"
   - TEST_TARGET="ci-geocoq"
   - TEST_TARGET="ci-fiat-crypto"
+  - TEST_TARGET="ci-fiat-parsers"
   - TEST_TARGET="ci-flocq"
   - TEST_TARGET="ci-hott"
   - TEST_TARGET="ci-iris-coq"
diff --git a/Makefile.ci b/Makefile.ci
index e4b5832f60..897318c4dd 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,5 +1,5 @@
 CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
-           ci-color ci-math-classes ci-tlc ci-fiat-crypto \
+           ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \
            ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
            ci-unimath
 
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
new file mode 100755
index 0000000000..15d73078fd
--- /dev/null
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+fiat_parsers_CI_BRANCH=master
+fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git
+
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat
+
+( cd fiat && make -j ${NJOBS} parsers )
-- 
cgit v1.2.3