diff options
| author | Jason Gross | 2019-12-02 15:33:12 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-12-26 13:52:55 -0500 |
| commit | f6a9b60b28c5cc9feb95d13411941a4604d6cae9 (patch) | |
| tree | 0872ac276a4a4040ba3b440f70f73c1504ccf6bb | |
| parent | 7d1138657904e5fe8ce1899daa001972ba820545 (diff) | |
Add non-utf8 timing test
This should have been running already, but it was forgotten in #9872
| -rwxr-xr-x | test-suite/coq-makefile/timing/precomputed-time-tests/run.sh | 1 |
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 |
