aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh
new file mode 100644
index 0000000000..69bd038b78
--- /dev/null
+++ b/dev/ci/user-overlays/13725-SkySkimmer-hint-rw-local.sh
@@ -0,0 +1 @@
+overlay equations https://github.com/SkySkimmer/Coq-Equations hint-rw-local 13725