diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-09 14:22:18 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-09 18:30:58 +0200 |
| commit | 73e91542293af304ff25db9d3ea5495a9aa95249 (patch) | |
| tree | 6cc38a97dc02eb30152c4d3ba4d6e6483a1fdfa6 /test-suite/misc | |
| parent | e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (diff) | |
test for coqc -o
Diffstat (limited to 'test-suite/misc')
| -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. |