aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross2019-12-02 15:33:12 -0500
committerJason Gross2019-12-26 13:52:55 -0500
commitf6a9b60b28c5cc9feb95d13411941a4604d6cae9 (patch)
tree0872ac276a4a4040ba3b440f70f73c1504ccf6bb
parent7d1138657904e5fe8ce1899daa001972ba820545 (diff)
Add non-utf8 timing test
This should have been running already, but it was forgotten in #9872
-rwxr-xr-xtest-suite/coq-makefile/timing/precomputed-time-tests/run.sh1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
index 9f3b648aa3..cfacf738a3 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
@@ -9,3 +9,4 @@ export COQLIB
./001-correct-diff-sorting-order/run.sh
./002-single-file-sorting/run.sh
+./003-non-utf8/run.sh