From 689893ab0b648c8385ce77ec47127676088fccd5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 30 Sep 2016 01:53:29 +0200
Subject: [pp] Implement n-ary glue.

---
 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 2b2017926..bd8509dbc 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -20,7 +20,7 @@ type block_type =
 type std_ppcmds =
   | Ppcmd_empty
   | Ppcmd_string of string
-  | Ppcmd_glue of std_ppcmds * std_ppcmds
+  | Ppcmd_glue of std_ppcmds list
   | Ppcmd_box  of block_type * std_ppcmds
   | Ppcmd_print_break of int * int
   | Ppcmd_white_space of int
-- 
cgit v1.2.3