From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 7 Apr 2003 15:58:38 +0000 (+0000)
Subject: ignore comments and blank line in servers file
X-Git-Tag: before_refactoring~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf78c8f8227bebbcaa6d6e2c51b26661c3dbfccf;p=helm.git

ignore comments and blank line in servers file
---

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 ()