diff options
Diffstat (limited to 'toplevel/whelp.ml4')
| -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 332d30536..5da85be03 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -177,7 +177,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 = subst_command_placeholder browser_cmd_fmt url in - let _ = run_command (fun x -> x) print_string command in () + let _ = CUnix.run_command (fun x -> x) print_string command in () let whelp_constr req c = let c = detype false [whelm_special] [] c in |