let delete_prefix prefix str =
let len = String.length str in
let plen = String.length prefix in
if (String.sub str 0 plen <> prefix)
then
(* XXX can a user make this happen? *)
raise Bad_path
else
Relpath(String.sub str (plen+1) (len-plen-1))