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 /kernel/nativecode.ml | |
| 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 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions