From 524eb4e7dcb18d622ebb99648862e5d08a972117 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 6 Oct 2020 00:42:08 +0200
Subject: Make description of Pp.pr_enum more precise + spacing in pp.ml.

---
 lib/pp.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.mli b/lib/pp.mli
index b3c2301d34..865f97166f 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -171,7 +171,7 @@ val prvecti_with_sep :
 
 val pr_enum : ('a -> t) -> 'a list -> t
 (** [pr_enum pr [a ; b ; ... ; c]] outputs
-    [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *)
+    [pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "and" ++ spc () ++ pr c]. *)
 
 val pr_sequence : ('a -> t) -> 'a list -> t
 (** Sequence of objects separated by space (unless an element is empty). *)
@@ -188,7 +188,6 @@ val pp_with          : Format.formatter -> t -> unit
 
 val string_of_ppcmds : t -> string
 
-
 (** Tag prefix to start a multi-token diff span *)
 val start_pfx : string
 
-- 
cgit v1.2.3