From 018b1517555fec38494d80124d9d7ca0bed6f9dc Mon Sep 17 00:00:00 2001 From: Marek Kubica Date: Fri, 24 Jul 2020 16:04:04 +0200 Subject: [PATCH] Remove unused interface This mli is not part of the public interface and also never touched by the compiler, so it could be completely wrong without anyone noticing. Better to delete it than to pretend this is of any use. --- lib/dune | 1 - lib/pretty.mli | 3 --- 2 files changed, 4 deletions(-) delete mode 100644 lib/pretty.mli diff --git a/lib/dune b/lib/dune index 5eaecea4..62660f5d 100644 --- a/lib/dune +++ b/lib/dune @@ -23,7 +23,6 @@ write.mli read.mli safe.mli - pretty.mli write2.mli common.mli util.mli diff --git a/lib/pretty.mli b/lib/pretty.mli deleted file mode 100644 index 2d1ad6b1..00000000 --- a/lib/pretty.mli +++ /dev/null @@ -1,3 +0,0 @@ -val pp : ?std:bool -> Format.formatter -> json -> unit -val to_string : ?std:bool -> json -> string -val to_channel : ?std:bool -> out_channel -> json -> unit