Add Path.drop_prefix
This commit is contained in:
parent
1de1ced82b
commit
829b85ec44
10
src/path.ml
10
src/path.ml
|
@ -429,3 +429,13 @@ let change_extension ~ext t =
|
|||
let extension = Filename.extension
|
||||
|
||||
let pp = Format.pp_print_string
|
||||
|
||||
let drop_prefix t ~prefix =
|
||||
let t = to_string t in
|
||||
let prefix =
|
||||
to_string (
|
||||
if String.is_suffix prefix ~suffix:"/" then
|
||||
prefix
|
||||
else
|
||||
prefix ^ "/") in
|
||||
String.drop_prefix t ~prefix
|
||||
|
|
|
@ -114,4 +114,12 @@ val change_extension : ext:string -> t -> t
|
|||
|
||||
val extension : t -> string
|
||||
|
||||
(** maintains the invariant:
|
||||
{[
|
||||
let suffix = Option.value_exn (Path.drop_prefix t ~prefix) in
|
||||
Path.relative prefix suffix = t
|
||||
]}
|
||||
*)
|
||||
val drop_prefix : t -> prefix:t -> string option
|
||||
|
||||
val pp : t Fmt.t
|
||||
|
|
Loading…
Reference in New Issue