From f7cf1f7e6f7f010e57e925e2fbb76a52fef74068 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 15:22:52 -0400
Subject: Add overlay for HoTT

The overlay for HoTT should be merged right after this PR.
---
 dev/ci/user-overlays/jasongross-numeral-notation-4.sh | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 dev/ci/user-overlays/jasongross-numeral-notation-4.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
new file mode 100644
index 0000000000..76aa37d380
--- /dev/null
+++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then
+    HoTT_CI_REF=fix-for-numeral-notations
+    HoTT_CI_GITURL=https://github.com/JasonGross/HoTT
+    HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive
+fi
-- 
cgit v1.2.3