]> matita.cs.unibo.it Git - helm.git/commitdiff
added the unregister method to the help page
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Feb 2005 11:46:31 +0000 (11:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Feb 2005 11:46:31 +0000 (11:46 +0000)
helm/ocaml/getter/http_getter_const.ml

index 944fc3ecab4e66ace659052edabb166a9d25a11d..f12d20f77bd8e79cd207b986c44c9f1a5595bf1c 100644 (file)
@@ -61,6 +61,9 @@ let usage_string configuration =
     <p>
       <b><kbd>register?uri=URI&amp;url=URL</kbd></b><br />
     </p>
+    <p>
+      <b><kbd>unregister?uri=URI&amp;url=URL</kbd></b><br />
+    </p>
     <p>
       <b><kbd>resolve?uri=URI</kbd></b><br />
     </p>