diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-05 02:01:56 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-07 22:56:56 +0100 |
| commit | 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 (patch) | |
| tree | 9af84a7fbc95a55c976c9d0529828cc87fb831b3 /plugins/extraction/json.ml | |
| parent | 69c4e7cfa0271f024b2178082e4be2e3ca3be263 (diff) | |
Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore
Diffstat (limited to 'plugins/extraction/json.ml')
0 files changed, 0 insertions, 0 deletions