diff options
| author | Gaëtan Gilbert | 2019-05-05 17:11:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-24 16:23:32 +0200 |
| commit | 46056cbe56f9c39fe3f8f5175aff9fd6427684b6 (patch) | |
| tree | 9c70ee243a2f5025bea4f7c8306d7cbd25f5d66f /kernel/type_errors.ml | |
| parent | 831639deec0ce88fca4ede4756815cf434088ac3 (diff) | |
Stop using pstate in global print queries
Using pstate makes no sense for printing global stuff
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions