From 8d9afb9c459ed7affdf6c0752ff6397e0281e0c3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 19 Sep 2019 16:31:33 -0400
Subject: Remove `rapply` tactic notation in favor of just the tactic

This increases backwards compatibility.  If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
---
 dev/ci/user-overlays/10760-JasonGross-more-rapply.sh | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 dev/ci/user-overlays/10760-JasonGross-more-rapply.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh b/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh
deleted file mode 100644
index c1cb1f15cd..0000000000
--- a/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10760" ] || [ "$CI_BRANCH" = "more-rapply" ]; then
-
-    math_classes_CI_BRANCH=fix-for-more-rapply-10760
-    math_classes_CI_REF=fix-for-more-rapply-10760
-    math_classes_CI_GITURL=https://github.com/JasonGross/math-classes
-
-fi
-- 
cgit v1.2.3