From 77b61ac3de351f462f113f8075c11518b2847935 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 29 Sep 2016 16:10:22 +0200
Subject: [pp] Make pp public to allow serialization.

---
 lib/pp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib/pp.ml')

diff --git a/lib/pp.ml b/lib/pp.ml
index 6d7bdf75e..140ad4e22 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -19,14 +19,14 @@ open Pp_control
    \end{description}
  *)
 
+type pp_tag = string list
+
 type block_type =
   | Pp_hbox   of int
   | Pp_vbox   of int
   | Pp_hvbox  of int
   | Pp_hovbox of int
 
-type pp_tag = string list
-
 type std_ppcmds =
   | Ppcmd_empty
   | Ppcmd_string of string
-- 
cgit v1.2.3