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  
    5050
    5151let make_request url =
    5252  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
    5357  let proxy =
    5458    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)
    5660      else None
    5761  in
    5862  let r = {