From 94c8f42eea1c36f582fe2390680de75634324c85 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 1 Aug 2019 15:14:42 +0200
Subject: [cleanup] Replace uses of UserError constructor, clarify exception
 names.

We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.

We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.

cc: #7560
---
 dev/ci/user-overlays/10660-ejgallego-errors+private.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10660-ejgallego-errors+private.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh
new file mode 100644
index 0000000000..21ff60493b
--- /dev/null
+++ b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then
+
+    coqhammer_CI_REF=errors+private
+    coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
+
+fi
-- 
cgit v1.2.3