diff options
Diffstat (limited to 'checker/include')
| -rw-r--r-- | checker/include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/include b/checker/include index b7d46d4b3..0b68da4b7 100644 --- a/checker/include +++ b/checker/include @@ -127,7 +127,7 @@ let mod_access m fld = ;; let parse_dp s = - make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s))) + make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s)) ;; let parse_sp s = let l = List.rev (Str.split(Str.regexp"\\.") s) in |