From 689893ab0b648c8385ce77ec47127676088fccd5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias 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