Skip to content

Commit

Permalink
Fix incorrect path normalization in coqdep on //..
Browse files Browse the repository at this point in the history
`x/y//..` would get normalized to `x/y` instead of `x`

Fix coq#19862
  • Loading branch information
SkySkimmer committed Dec 2, 2024
1 parent beb35a7 commit 57102a2
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions tools/coqdep/lib/file_util.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,12 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

let re_delim = Str.regexp (if Sys.win32 then "[/\\]+" else "/+" )

let to_relative_path : string -> string = fun full_path ->
if Filename.is_relative full_path then full_path else
let re_delim = if Sys.win32 then "[/\\]" else "/" in
let cwd = Str.split_delim (Str.regexp re_delim) (Sys.getcwd ()) in
let path = Str.split_delim (Str.regexp re_delim) full_path in
let cwd = Str.split_delim re_delim (Sys.getcwd ()) in
let path = Str.split_delim re_delim full_path in
let rec remove_common_prefix l1 l2 =
match (l1, l2) with
| (x1 :: l1, x2 :: l2) when x1 = x2 -> remove_common_prefix l1 l2
Expand All @@ -23,8 +24,7 @@ let to_relative_path : string -> string = fun full_path ->
List.fold_left add_parent path cwd

let normalize_path : string -> string = fun path ->
let re_delim = if Sys.win32 then "[/\\]" else "/" in
let path = Str.split_delim (Str.regexp re_delim) path in
let path = Str.split_delim re_delim path in
let rec normalize acc path =
match (path, acc) with
| ([] , _ ) -> List.rev acc
Expand Down

0 comments on commit 57102a2

Please sign in to comment.