diff options
Diffstat (limited to 'ci/compile-tests/bin/coqc-delayed')
| -rwxr-xr-x | ci/compile-tests/bin/coqc-delayed | 3 |
1 files changed, 3 insertions, 0 deletions
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 "$*" |