diff options
| author | Maxime Dénès | 2019-10-21 15:50:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-21 15:50:26 +0200 |
| commit | 50e3fd2b6f30ab209200950fd5a804a18b47288f (patch) | |
| tree | 21085d5efc424c36d69963eab3fe123f0a261422 /test-suite/misc | |
| parent | c6056bdc54d02dc5c6a91aeacb13460e8dd365e3 (diff) | |
| parent | cd03a27b917dedc129af980a6099b20134cba9f5 (diff) | |
Merge PR #10857: Fix votour after the change of representation of opaques.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Diffstat (limited to 'test-suite/misc')
| -rwxr-xr-x | test-suite/misc/votour.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/misc/votour.sh b/test-suite/misc/votour.sh new file mode 100755 index 0000000000..ac26aed49b --- /dev/null +++ b/test-suite/misc/votour.sh @@ -0,0 +1,3 @@ +command -v "${BIN}votour" || { echo "Missing votour"; exit 1; } + +"${BIN}votour" prerequisite/ssr_mini_mathcomp.vo < /dev/null |