diff options
Diffstat (limited to 'devtools/credits.pl')
| -rwxr-xr-x | devtools/credits.pl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/devtools/credits.pl b/devtools/credits.pl index 7a7766657b..6a4b97b89d 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -553,7 +553,9 @@ begin_credits("Credits"); begin_section("DreamWeb"); add_person("Torbjörn Andersson", "eriktorbjorn", ""); add_person("Bertrand Augereau", "Tramb", ""); + add_person("Filippos Karapetis", "[md5]", ""); add_person("Vladimir Menshakov", "whoozle", "(retired)"); + add_person("Willem Jan Palenstijn", "wjp", ""); end_section(); begin_section("Gob"); |