diff options
| author | Jason Gross | 2019-03-31 10:40:56 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-03-31 14:09:06 -0400 |
| commit | 2acd04d6d7d608920dd93b0a602e3214ffeb9ae5 (patch) | |
| tree | 2cb75c49a849fbd3d0519de8bfe4cdf67c55d615 /.gitignore | |
| parent | 4713f5c22bb21d341de32498f2a49d92aa1fc08c (diff) | |
[pretty-timing scripts] Don't barf on non-utf-8
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8. We hereby assume that all file paths are valid UTF-8.
We also now actually test both python2 and python3 on the CI.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 23e305892e..8fd9fc614c 100644 --- a/.gitignore +++ b/.gitignore @@ -64,6 +64,8 @@ time-of-build.log time-of-build-pretty.log time-of-build-before.log time-of-build-after.log +time-of-build-pretty.log2 +time-of-build-pretty.log3 .csdp.cache test-suite/.lia.cache test-suite/.nra.cache |