diff options
| author | Pierre Letouzey | 2014-01-30 15:49:15 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-01-30 18:36:50 +0100 |
| commit | 2fa5d8befba9ef24629233a3620494760583f75f (patch) | |
| tree | f7435fbe5f29a49734796b3e336013e3f53d208c /toplevel | |
| parent | 84b09aae2c727877c98e02508ddcd3b6a3ee9db7 (diff) | |
CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/whelp.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 8870254182..79673df32b 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -174,7 +174,7 @@ let make_string f x = Buffer.reset b; f x; Buffer.contents b let send_whelp req s = let url = make_whelp_request req s in let command = Util.subst_command_placeholder browser_cmd_fmt url in - let _ = CUnix.run_command (fun x -> x) print_string command in () + let _ = CUnix.run_command ~hook:print_string command in () let whelp_constr req c = let c = detype false [whelm_special] [] c in |