bugfix in uri's: missing "/" added to baseuri's where necessary

[helm.git] / helm / software / helena / src / common / options.ml

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 8cc200ad92b025b9063e171f6a6fe4782aecfbad..a2c749872e525f612b610152089373d35df123e2 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -9,6 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module F = Filename
 module C = Cps
 
 type uri_generator = string -> string
@@ -49,11 +50,11 @@ let kernel_id () =
    id ^ si
 
 let get_baseuri () =
-   String.concat "/" ["ld:"; kernel_id (); !cover ]
+   String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
 
 let get_mk_uri () =
    let bu = get_baseuri () in
-   fun s -> bu ^ "/" ^ s ^ ".ld"
+   fun s -> F.concat bu (s ^ ".ld")
 
 let clear () =
    xdir := ""; kernel := Brg; si := false; cover := "";