diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index e5edce660e..4cf9c1ba22 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -240,3 +240,24 @@ let rec print_list print fmt = function | [] -> () | [x] -> print fmt x | x :: r -> print fmt x; print_list print fmt r + + +let run_command f c = + let result = Buffer.create 127 in + let cin,cout,cerr = Unix.open_process_full c [||] in + let buff = String.make 127 ' ' in + let buffe = String.make 127 ' ' in + let n = ref 0 in + let ne = ref 0 in + + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; + !n+ !ne <> 0 + do + let r = String.sub buff 0 !n in + f r; + Buffer.add_string result r; + let r = String.sub buffe 0 !ne in + f r; + Buffer.add_string result r + done; + (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) |
