From 745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 15 Aug 2017 14:47:15 +0200
Subject: Improving spacing in printing disjunctive patterns.

Adding a space before the bar separating disjunctive patterns.
Removing an extra space after the bar for inner disjunctive patterns.
---
 lib/pp.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 2d11cad86..d9be1c5ce 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -120,6 +120,9 @@ val pr_semicolon : unit -> t
 val pr_bar : unit -> t
 (** Well-spaced pipe bar. *)
 
+val pr_spcbar : unit -> t
+(** Pipe bar with space before and after. *)
+
 val pr_arg : ('a -> t) -> 'a -> t
 (** Adds a space in front of its argument. *)
 
-- 
cgit v1.2.3