aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/plugin2
diff options
context:
space:
mode:
authorEnrico Tassi2019-10-28 12:51:49 +0100
committerPierre-Marie Pédrot2019-11-01 12:17:08 +0100
commit76c72065a10381d91317c12436e3d6c1cd2e7348 (patch)
tree1eb6278ece39d0b025654cabca82ff45d48ed0d3 /test-suite/coq-makefile/plugin2
parent69657170aa1ac065765de00411e04400942ae28a (diff)
[test-suite] acknowledge coq_mafile installs .vos
Diffstat (limited to 'test-suite/coq-makefile/plugin2')
-rwxr-xr-xtest-suite/coq-makefile/plugin2/run.sh1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index 1e2bd979b3..cd47187582 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -22,5 +22,6 @@ sort > desired <<EOT
./test/test_plugin.cmxs
./test/test.v
./test/test.vo
+./test/test.vos
EOT
exec diff -u desired actual