From 93b319688225c2e3e38ebc389feff2523b76ab26 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 6 Jan 2020 16:52:54 +0100
Subject: [PATCH] [gui] Use actual path of files and not their prettified
versions.
---
src/plugins/gui/file_manager.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 28bdb46df11..20b4da69398 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -23,7 +23,7 @@
let add_files (host_window: Design.main_window_extension_points) =
Gtk_helper.source_files_chooser
(host_window :> Gtk_helper.source_files_chooser_host)
- (List.map Filepath.Normalized.to_pretty_string (Kernel.Files.get ()))
+ (Kernel.Files.get () :> string list)
(fun filenames ->
Kernel.Files.set (List.map Datatype.Filepath.of_string filenames);
if Ast.is_computed () then
--
GitLab