From 669b4859f95a15fb994c1879175c76b760d58cc1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 7 May 2020 16:10:39 +0200
Subject: [PATCH] add new author
---
opam/opam | 1 +
src/plugins/gui/help_manager.ml | 1 +
2 files changed, 2 insertions(+)
diff --git a/opam/opam b/opam/opam
index 59c2ae9d96f..042f85254d7 100644
--- a/opam/opam
+++ b/opam/opam
@@ -19,6 +19,7 @@ authors: [
"Julien Crétin"
"Pascal Cuoq"
"Zaynah Dargaye"
+ "Basile Desloges"
"Jean-Christophe Filliâtre"
"Philippe Herrmann"
"Maxime Jacquemin"
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index 68983f58f9e..286541b637b 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -37,6 +37,7 @@ let show main_ui =
"Julien Crétin";
"Pascal Cuoq";
"Zaynah Dargaye";
+ "Basile Desloges";
"Jean-Christophe Filliâtre";
"Philippe Herrmann";
"Maxime Jacquemin";
--
GitLab