]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_misc.mli
- added functions "add_line" and "remove_line" to edit line oriented files
[helm.git] / helm / http_getter / http_getter_misc.mli
index 2047cf204b852736782672a1f8152b1a916c46ce..c6e2e72c6e18c873fc48fd3dfb5b82ac7fb56ad4 100644 (file)
@@ -73,3 +73,10 @@ val http_get: string -> string option
   remote resources fetched via HTTP GET requests *)
 val http_get_iter_buf: callback:(string -> unit) -> string -> unit
 
+  (** add a line to a file (specified by name) _after_ a given line (defaults to
+  last line). *)
+val add_line: fname:string -> ?position:int -> string -> unit
+  (** remove a line, if any, from a file specified by line number (0 based, i.e.
+  first line of file is line 0) *)
+val remove_line: fname:string -> int -> unit
+