From 9113815578286d1d887df48f4f03870d2d8a128c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Nov 2017 19:32:52 +0100
Subject: Adding overlay for ltac2.

---
 .../06158-herbelin-master+fix-pr6158-ltac-value-printer.sh            | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
new file mode 100644
index 0000000000..cdca8e525a
--- /dev/null
+++ b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then
+    ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer
+    ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git
+fi
-- 
cgit v1.2.3