diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-05 02:12:36 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-07 22:56:56 +0100 |
| commit | df14dac0e6e9d9819dcc3b1601e150af7c142597 (patch) | |
| tree | b2cd633c679810d0eae8a9441b11ac2f9902c1a8 /plugins/extraction/json.ml | |
| parent | 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 (diff) | |
Extraction cosmetic: no whitespaces in printing empty modules
Diffstat (limited to 'plugins/extraction/json.ml')
0 files changed, 0 insertions, 0 deletions