diff options
| author | Pierre-Marie Pédrot | 2016-06-02 18:00:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-02 18:00:30 +0200 |
| commit | 71b64cc5ec5ab0d70d437ec4542c5903f43063cb (patch) | |
| tree | 440fb8e51d1fe118d866d0c620a86724e3c6eae8 /lib/richpp.ml | |
| parent | 2d2d86c165cac7b051da1c5079d614a76550a20c (diff) | |
| parent | 318fc2c04df1e73cc8a178d4fc1ce8bf5543649b (diff) | |
Move XML serialization to ide/ folder.
Diffstat (limited to 'lib/richpp.ml')
| -rw-r--r-- | lib/richpp.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/richpp.ml b/lib/richpp.ml index fe3edd99ca..a98273edb2 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -194,7 +194,3 @@ let raw_print xml = let () = print xml in Buffer.contents buf -let of_richpp x = Element ("richpp", [], [x]) -let to_richpp xml = match xml with -| Element ("richpp", [], [x]) -> x -| _ -> raise Serialize.Marshal_error |