From 27e0cfd73dfa63f1b9333413dd5dd95b5815440e Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 2 Aug 2019 10:58:47 +0200
Subject: [PATCH] lint
---
src/plugins/gui/design.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index d5693f4e0b9..287a5d8e0b0 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1864,7 +1864,7 @@ let toplevel play =
(fun f -> ignore (Glib.Timeout.add ~ms:50 ~callback:f));
let project_name = Gui_parameters.Project_name.get () in
if project_name = "" then
- Project.set_current_as_last_created ()
+ Project.set_current_as_last_created ()
else
Project.set_current (Project.from_unique_name project_name);
Ast.compute ()
--
GitLab