From d306f5428db0d034aea55d3f0699c67c1f296cc1 Mon Sep 17 00:00:00 2001
From: JPR
Date: Thu, 23 May 2019 23:28:55 +0200
Subject: Fixing typos - Part 3

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

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 8b3a07d4b2..bc20a66824 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -18,7 +18,7 @@
 (* to interpret.                                                        *)
 (*                                                                      *)
 (* The datatype has a public view to allow serialization or advanced    *)
-(* uses, however regular users are _strongly_ warned against its use,    *)
+(* uses, however regular users are _strongly_ warned against its use,   *)
 (* they should instead rely on the available functions below.           *)
 (*                                                                      *)
 (* Box order and number is indeed an important factor. Try to create    *)
-- 
cgit v1.2.3