From cc3ded87f0f440eac2746d59b7aeba60ca9f691f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Dec 2019 11:41:33 +0100
Subject: Rename files with Class in their name to make their role clearer.

We restrict to those that are actually related to typeclasses, and
perform the following renamings:

Classops --> Coercionops
Class --> ComCoercion
---
 dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
new file mode 100644
index 0000000000..a95170a455
--- /dev/null
+++ b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then
+
+    elpi_CI_REF=rename-class-files
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    mtac2_CI_REF=rename-class-files
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
-- 
cgit v1.2.3