aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Printlines.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-03-10 13:35:48 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-03-10 13:35:48 +0100
commit5b05d3668571bd9b748b781b0cc29ae10f745f61 (patch)
treeaa235b80ff0666c34332be46664ae289d8afaa2c /lib/Printlines.mli
parent272087e1bc62bead1d1e1bea3d64e12d013eea37 (diff)
downloadcompcert-kvx-5b05d3668571bd9b748b781b0cc29ae10f745f61.tar.gz
compcert-kvx-5b05d3668571bd9b748b781b0cc29ae10f745f61.zip
Code cleanup.
Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
Diffstat (limited to 'lib/Printlines.mli')
-rw-r--r--lib/Printlines.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/Printlines.mli b/lib/Printlines.mli
index 79201f86..545eb033 100644
--- a/lib/Printlines.mli
+++ b/lib/Printlines.mli
@@ -20,8 +20,10 @@ type filebuf
val openfile: string -> filebuf
(** Open the file with the given name. *)
+
val close: filebuf -> unit
(** Close the file underlying the given buffer. *)
+
val copy: out_channel -> string -> filebuf -> int -> int -> unit
(** [copy oc pref buf first last] copies lines number [first]
to [last], included, to the channel [oc]. Each line is