diff options
| -rwxr-xr-x | devtools/credits.pl | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/devtools/credits.pl b/devtools/credits.pl index ba209e8591..2833236e75 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -590,13 +590,6 @@ begin_credits("Credits"); add_person("Paul Gilbert", "dreammaster", ""); end_section(); - begin_section("M4"); - add_person("Torbjörn Andersson", "eriktorbjorn", ""); - add_person("Paul Gilbert", "dreammaster", ""); - add_person("Benjamin Haisch", "john_doe", ""); - add_person("Filippos Karapetis", "[md5]", ""); - end_section(); - begin_section("MADE"); add_person("Benjamin Haisch", "john_doe", ""); add_person("Filippos Karapetis", "[md5]", ""); |