From: Stefano Zacchiroli Date: Mon, 7 Apr 2003 16:06:12 +0000 (+0000) Subject: added a TODO bug comment X-Git-Tag: before_refactoring~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=942c35c7f24ca9f1413cc346970aa80b54730e94;p=helm.git added a TODO bug comment --- diff --git a/helm/http_getter/http_getter_env.ml b/helm/http_getter/http_getter_env.ml index 7b59cf122..542692795 100644 --- a/helm/http_getter/http_getter_env.ml +++ b/helm/http_getter/http_getter_env.ml @@ -3,8 +3,7 @@ * Stefano Zacchiroli * for the HELM Team http://helm.cs.unibo.it/ * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science + * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or @@ -77,6 +76,10 @@ let safe_getenv ?(from = Both) var = | v -> return_value var v))) let servers_file = safe_getenv "HTTP_GETTER_SERVERS_FILE" + + (* TODO BUG HERE: is commented lines are included in the servers file the + server index (used for example by the remove_server method) gets out of sync! + *) let parse_servers () = List.rev (Http_getter_misc.fold_file (fun servers line ->