From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 test-suite/misc/coqc_dash_o.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100755 test-suite/misc/coqc_dash_o.sh

(limited to 'test-suite/misc/coqc_dash_o.sh')

diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh
new file mode 100755
index 00000000..0ae7873f
--- /dev/null
+++ b/test-suite/misc/coqc_dash_o.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+DOUT=misc/tmp_coqc_dash_o/
+OUT=${DOUT}coqc_dash_o.vo
+
+
+mkdir -p "${DOUT}"
+rm -f "${OUT}"
+$coqc misc/coqc_dash_o.v -o "${OUT}"
+if [ ! -f "${OUT}" ]; then
+  printf "coqc -o not working"
+  exit 1
+fi
+rm -fr "${DOUT}"
+exit 0
-- 
cgit v1.2.3