Huge commit with several changes:

[helm.git] / helm / software / components / urimanager / uriManager.ml

diff --git a/helm/software/components/urimanager/uriManager.ml b/helm/software/components/urimanager/uriManager.ml
index 9107994a1d31803bb45b602476225005a3a71bc1..2d099a4e9748bf64cae26ef76bf6361ce9986821 100644 (file)
--- a/helm/software/components/urimanager/uriManager.ml
+++ b/helm/software/components/urimanager/uriManager.ml
@@ -193,7 +193,6 @@ let bodyuri_of_uri (uri, _) =
 
 let ind_uri_split ((s, _) as uri) =
     let noxp = strip_xpointer uri in
-    let length = String.length s in
     try 
       (let arg_index = String.rindex s '(' in
        try