]> matita.cs.unibo.it Git - helm.git/commitdiff
ignore comments and blank line in servers file
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 15:58:38 +0000 (15:58 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 15:58:38 +0000 (15:58 +0000)
helm/http_getter/ChangeLog
helm/http_getter/http_getter_env.ml

index a352d45d22e8b3308be61c6868af587f29457d4b..cd6f55bbd400bece4f11d57ae2e007d50542fdcf 100644 (file)
@@ -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
 
index a531cfa7576952c2998f6e1cd1500ec8129dffef..7b59cf1220f6c8c63eeecd8755d6bcdc7afb638d 100644 (file)
@@ -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 ()