From cf78c8f8227bebbcaa6d6e2c51b26661c3dbfccf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 7 Apr 2003 15:58:38 +0000 Subject: [PATCH] ignore comments and blank line in servers file --- helm/http_getter/ChangeLog | 1 + helm/http_getter/http_getter_env.ml | 8 ++++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/http_getter/ChangeLog b/helm/http_getter/ChangeLog index a352d45d2..cd6f55bbd 100644 --- a/helm/http_getter/ChangeLog +++ b/helm/http_getter/ChangeLog @@ -1,3 +1,4 @@ +- ignore comments and blank lines in servers file - added "list_servers", "add_server", "remove_server" methods - bugfix: multiple definition of URI by different servers are now permitted diff --git a/helm/http_getter/http_getter_env.ml b/helm/http_getter/http_getter_env.ml index a531cfa75..7b59cf122 100644 --- a/helm/http_getter/http_getter_env.ml +++ b/helm/http_getter/http_getter_env.ml @@ -78,8 +78,12 @@ let safe_getenv ?(from = Both) var = let servers_file = safe_getenv "HTTP_GETTER_SERVERS_FILE" let parse_servers () = - (let cons hd tl = hd @ [ tl ] in - Http_getter_misc.fold_file cons [] servers_file) + List.rev (Http_getter_misc.fold_file + (fun servers line -> + if Http_getter_misc.is_blank_line line then servers else line::servers) + [] + servers_file) +;; let servers = ref (parse_servers ()) let reload_servers () = servers := parse_servers () -- 2.39.2