]> matita.cs.unibo.it Git - helm.git/commitdiff
added backtick function
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 6 Jul 2005 15:49:55 +0000 (15:49 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 6 Jul 2005 15:49:55 +0000 (15:49 +0000)
helm/ocaml/getter/http_getter_misc.ml
helm/ocaml/getter/http_getter_misc.mli

index 85b87cb93438c1c097076bd1bf602c1fb3db8f27..b7b52bbf64309da80028b1b5cfd47fff7c31c615 100644 (file)
@@ -305,3 +305,9 @@ let temp_file_of_uri uri =
   let user = try Unix.getlogin () with _ -> "" in
   Filename.open_temp_file (user ^ flat_string uri ".-=:;!?/&" '_') ""
 
+let backtick cmd =
+  let ic = Unix.open_process_in cmd in
+  let res = input_line ic in
+  ignore (Unix.close_process_in ic);
+  res
+
index e9086e8d1128957b81cba7c01633d3d1fcd4669d..e9b013ebd496738596e7d3afbbe46f0877b0164b 100644 (file)
@@ -97,3 +97,6 @@ val extension: string -> string  (** @return string part after rightmost "." *)
 
 val temp_file_of_uri: string -> string * out_channel
 
+  (** execute a command and return first line of what it prints on stdout *)
+val backtick: string -> string
+