diff options
| author | Maxime Dénès | 2017-03-29 17:52:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-29 17:52:38 +0200 |
| commit | 486afa4ccf6a3b84badfaa30282781a33a29b619 (patch) | |
| tree | dc8c7642e9a0fc6e4b19fae09e9ba9acfd7eca64 | |
| parent | 45985baf2262504a9fb8f24e7960caa9f11d29f3 (diff) | |
| parent | 026edb0b10eaf96f7f9f4e806bd3a0fa19b29407 (diff) | |
Merge PR#525: [ide] Fix typo in pp serialization.
| -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 5f80d68974..d7950e5fd5 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)] |