http_getter reimplemented from scratch

[helm.git] / helm / interface / pxpUriResolver.ml

diff --git a/helm/interface/pxpUriResolver.ml b/helm/interface/pxpUriResolver.ml
index 6ebbf71bd4bf02165b140e00dc7cd292e4734578..ad8713cf371031a911c5cbc88795fc5651e78e4c 100644 (file)
--- a/helm/interface/pxpUriResolver.ml
+++ b/helm/interface/pxpUriResolver.ml
@@ -10,11 +10,11 @@
 
 let resolve =
  function
-    "http://localhost:8081/getdtd?url=cic.dtd" ->
+    "http://localhost:8081/getdtd?uri=cic.dtd" ->
      Configuration.dtd_dir ^ "/cic.dtd"
-  | "http://localhost:8081/getdtd?url=maththeory.dtd" ->
+  | "http://localhost:8081/getdtd?uri=maththeory.dtd" ->
      Configuration.dtd_dir ^ "/maththeory.dtd"
-  | "http://localhost:8081/getdtd?url=annotations.dtd" ->
+  | "http://localhost:8081/getdtd?uri=annotations.dtd" ->
      Configuration.dtd_dir ^ "/annotations.dtd"
   | s  -> s
 ;;