diff options
-rwxr-xr-x | test-suite/misc/coqc_dash_o.sh | 15 | ||||
-rw-r--r-- | test-suite/misc/coqc_dash_o.v | 1 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh new file mode 100755 index 000000000..f303214b9 --- /dev/null +++ b/test-suite/misc/coqc_dash_o.sh @@ -0,0 +1,15 @@ +#!/bin/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 diff --git a/test-suite/misc/coqc_dash_o.v b/test-suite/misc/coqc_dash_o.v new file mode 100644 index 000000000..7426dff1a --- /dev/null +++ b/test-suite/misc/coqc_dash_o.v @@ -0,0 +1 @@ +Definition x := nat. |