]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 22cc7ae)
comment mangling
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 27 Dec 2002 10:48:13 +0000 (10:48 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 27 Dec 2002 10:48:13 +0000 (10:48 +0000)
helm/http_getter/http_getter_const.ml patch | blob | history

diff --git a/helm/http_getter/http_getter_const.ml b/helm/http_getter/http_getter_const.ml
index 93c2d5d6a8237fa5fedaece08f7bcfcf2f323407..b3d389aebda5fd8fe8b2013202afe8de203d2498 100644 (file)
--- a/helm/http_getter/http_getter_const.ml
+++ b/helm/http_getter/http_getter_const.ml
@@ -24,7 +24,7 @@
  *  http://cs.unibo.it/helm/.
  *)
 
-  (* TODO *)
+  (* TODO provide a better usage string *)
 let usage_string =
 "
 <html>
Unnamed repository; edit this file 'description' to name the repository.