From 0d731606bee81b2d73895a23b69e84796ea7e4e7 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Fri, 1 Jan 2021 22:56:48 +0100
Subject: add Coq compile test for a delayed require

---
 ci/compile-tests/bin/coqc-delayed | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100755 ci/compile-tests/bin/coqc-delayed

(limited to 'ci/compile-tests/bin/coqc-delayed')

diff --git a/ci/compile-tests/bin/coqc-delayed b/ci/compile-tests/bin/coqc-delayed
new file mode 100755
index 00000000..26c92805
--- /dev/null
+++ b/ci/compile-tests/bin/coqc-delayed
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+exec compile-test-start-delayed coqc-delay coqc "$*"
-- 
cgit v1.2.3