From 8d89102e84d41956fb1359089d573cc64d7838ca Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 25 Jun 2018 13:31:50 +0200
Subject: Add overlay for elpi

---
 dev/ci/user-overlays/07863-rm-sorts-contents.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/07863-rm-sorts-contents.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/07863-rm-sorts-contents.sh b/dev/ci/user-overlays/07863-rm-sorts-contents.sh
new file mode 100644
index 000000000..374a61484
--- /dev/null
+++ b/dev/ci/user-overlays/07863-rm-sorts-contents.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7863" ] || [ "$CI_BRANCH" = "rm-sorts-contents" ]; then
+    Elpi_CI_BRANCH=fix-sorts-contents
+    Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
+fi
-- 
cgit v1.2.3