From: Stefano Zacchiroli <zack@upsilon.cc>
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/?p=helm.git;a=commitdiff_plain;h=942c35c7f24ca9f1413cc346970aa80b54730e94

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 <zack@cs.unibo.it>
  *    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 ->