diff options
Diffstat (limited to 'utils/build_path_prefix_map.mli')
| -rw-r--r-- | utils/build_path_prefix_map.mli | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/utils/build_path_prefix_map.mli b/utils/build_path_prefix_map.mli index dbcc8dc16f..d8ec9caf4d 100644 --- a/utils/build_path_prefix_map.mli +++ b/utils/build_path_prefix_map.mli @@ -18,6 +18,9 @@ {b Warning:} this module is unstable and part of {{!Compiler_libs}compiler-libs}. + See + {{: https://reproducible-builds.org/specs/build-path-prefix-map/ } + the BUILD_PATH_PREFIX_MAP spec} *) @@ -38,10 +41,21 @@ type map = pair option list val encode_map : map -> string val decode_map : string -> (map, error_message) result -val rewrite_opt : map -> path -> path option -(** [rewrite_opt map path] tries to find a source in [map] +val rewrite_first : map -> path -> path option +(** [rewrite_first map path] tries to find a source in [map] that is a prefix of the input [path]. If it succeeds, it replaces this prefix with the corresponding target. If it fails, it just returns [None]. *) +val rewrite_all : map -> path -> path list +(** [rewrite_all map path] finds all sources in [map] + that are a prefix of the input [path]. For each matching + source, in priority order, it replaces this prefix with + the corresponding target and adds the result to + the returned list. + If there are no matches, it just returns [[]]. *) + val rewrite : map -> path -> path +(** [rewrite path] uses [rewrite_first] to try to find a + mapping for path. If found, it returns that, otherwise + it just returns [path]. *) |