diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index cee7fa0528..5bf5391d3b 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -25,7 +25,6 @@ type std_ppcmds = | Ppcmd_tag of pp_tag * std_ppcmds (* Are those redundant? *) | Ppcmd_print_break of int * int - | Ppcmd_white_space of int | Ppcmd_force_newline | Ppcmd_comment of string list |