diff options
| -rwxr-xr-x | devtools/credits.pl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/devtools/credits.pl b/devtools/credits.pl index 41c2d4f162..6f58528d57 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -877,6 +877,10 @@ begin_credits("Credits"); add_person("Andre Heider", "dhewg", ""); end_section(); + begin_section("Raspberry Pi"); + add_person("Manuel Alfayate", "vanfanel", ""); + end_section(); + end_section(); begin_section("Other subsystems"); |