From b1cfb65fbf7c11cb5b9acc8039bcf5e36882a685 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 14 Dec 2015 11:11:49 +0100 Subject: Extraction: cosmetically avoid generating spaces on empty lines --- plugins/extraction/extract_env.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/extract_env.ml') 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. *) -- cgit v1.2.3