From ca5aaa579d9fe87e999f543db0dcb66d2b78032c Mon Sep 17 00:00:00 2001
From: whonore
Date: Mon, 20 Jul 2020 14:35:49 -0400
Subject: Add Coqtail to CI

---
 dev/ci/ci-coqtail.sh | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100755 dev/ci/ci-coqtail.sh

(limited to 'dev/ci/ci-coqtail.sh')

diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh
new file mode 100755
index 0000000000..b8b5c6c724
--- /dev/null
+++ b/dev/ci/ci-coqtail.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coqtail
+
+( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py )
-- 
cgit v1.2.3