Ticket #26292: patch-gui-guiHtml.diff
File patch-gui-guiHtml.diff, 670 bytes (added by mcklaren@…, 14 years ago) |
---|
-
src/gtk2/gui/guiHtml.ml
old new 50 50 51 51 let make_request url = 52 52 let module H = Http_client in 53 let auth = match !!O.gtk_connection_http_proxy_login with 54 | "" -> None 55 | _ -> Some (!!O.gtk_connection_http_proxy_login, !!O.gtk_connection_http_proxy_password) 56 in 53 57 let proxy = 54 58 if !!O.gtk_connection_http_use_proxy 55 then Some (!!O.gtk_connection_http_proxy_server, !!O.gtk_connection_http_proxy_port )59 then Some (!!O.gtk_connection_http_proxy_server, !!O.gtk_connection_http_proxy_port, auth) 56 60 else None 57 61 in 58 62 let r = {