diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-29 14:27:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-29 14:27:39 +0200 |
| commit | 026edb0b10eaf96f7f9f4e806bd3a0fa19b29407 (patch) | |
| tree | 1af15480c121aa482ab463f0b5ed2c05dc22b217 /ide | |
| parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) | |
[ide] Fix typo in pp serialization.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/xmlprotocol.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 5f80d6897..d7950e5fd 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -111,7 +111,7 @@ let to_box = let open Pp in ) let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with - | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] + | Ppcmd_empty -> constructor "ppdoc" "empty" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] |