diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-14 11:11:49 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-14 11:11:49 +0100 |
| commit | b1cfb65fbf7c11cb5b9acc8039bcf5e36882a685 (patch) | |
| tree | d7545035042e78501102933fd47fc95255c4a829 /plugins/extraction/extract_env.ml | |
| parent | a2a81cec811a8257e47ceb1b9ea3de6d1c2607ee (diff) | |
Extraction: cosmetically avoid generating spaces on empty lines
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3d32398ff..7014df83f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -458,7 +458,7 @@ let print_one_decl struc mp decl = push_visible mp []; let ans = d.pp_decl decl in pop_visible (); - ans + v 0 ans (*s Extraction of a ml struct to a file. *) |