Skip to content
Snippets Groups Projects
Commit 52eba442 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'fix/andre/filepath-relative-symbolic-name' into 'master'

[kernel] avoid special case when prettifying paths inside PWD

See merge request frama-c/frama-c!4706
parents 5f4981b1 0b62d255
No related branches found
No related tags found
No related merge requests found
......@@ -233,14 +233,7 @@ let pretty file_name =
skip_dot file_name
else
let path = insert cwd file_name in
let file_name = path.path_name in
let cwd_name = cwd.path_name in
if String.starts_with ~prefix:cwd_name file_name && cwd_name <> file_name
then
let n = 1 + String.length cwd_name in
String.sub file_name n (String.length file_name - n)
else
skip_dot (add_path path)
skip_dot (add_path path)
(* -------------------------------------------------------------------------- *)
(* --- Relative Paths --- *)
......
......@@ -4,21 +4,21 @@ Basic case
$ dune exec -- frama-c
[kernel] IS_SET false
[dirs] path (dir)
[dirs] Found: _build/install/default/share/frama-c/share/dirs/path
[dirs] Found: FRAMAC_SHARE/dirs/path
[dirs] Path (.)
[dirs] Found: _build/install/default/share/frama-c/share/dirs/path
[dirs] Found: FRAMAC_SHARE/dirs/path
[dirs] path/file.txt (file)
[dirs] Found: _build/install/default/share/frama-c/share/dirs/path/file.txt
[dirs] Found: FRAMAC_SHARE/dirs/path/file.txt
[dirs] Path (file)
[dirs] Found: _build/install/default/share/frama-c/share/dirs/path/file.txt
[dirs] Found: FRAMAC_SHARE/dirs/path/file.txt
[dirs] foo (dir)
[dirs] User Error: Could not find directory foo in Frama-C/directories share
[dirs] foo.txt (file)
[dirs] User Error: Could not find file foo.txt in Frama-C/directories share
[dirs] path (file)
[dirs] User Error: _build/install/default/share/frama-c/share/dirs/path is expected to be a file
[dirs] User Error: FRAMAC_SHARE/dirs/path is expected to be a file
[dirs] path/file.txt
[dirs] User Error: _build/install/default/share/frama-c/share/dirs/path/file.txt is expected to be a directory
[dirs] User Error: FRAMAC_SHARE/dirs/path/file.txt is expected to be a directory
With option
$ cp -r share copied
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment