From 7bee3feb2a2c2fd723fd182035e0e6a5482e237c Mon Sep 17 00:00:00 2001 From: Jan Rochel <jan.rochel@cea.fr> Date: Fri, 12 May 2023 15:01:06 +0200 Subject: [PATCH] add Jan Rochel to authors --- opam | 1 + src/plugins/gui/help_manager.ml | 1 + 2 files changed, 2 insertions(+) diff --git a/opam b/opam index a72a1319bd1..1483c4466ca 100644 --- a/opam +++ b/opam @@ -61,6 +61,7 @@ authors: [ "Armand Puccetti" "Félix Ridoux" "Virgile Robles" + "Jan Rochel" "Muriel Roger" "Julien Signoles" "Nicolas Stouls" diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml index 9d08557f5be..d0e1fedf9ea 100644 --- a/src/plugins/gui/help_manager.ml +++ b/src/plugins/gui/help_manager.ml @@ -64,6 +64,7 @@ let show main_ui = "Armand Puccetti"; "Félix Ridoux"; "Virgile Robles"; + "Jan Rochel"; "Muriel Roger"; "Julien Signoles"; "Nicolas Stouls"; -- GitLab