diff options
| -rwxr-xr-x | devtools/credits.pl | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/devtools/credits.pl b/devtools/credits.pl index ad011b7248..3cfa7b748c 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -623,6 +623,13 @@ begin_credits("Credits"); begin_section("Fullpipe"); add_person("Eugene Sandulenko", "sev", ""); end_section(); + + begin_section("Gargoyle"); + add_person("Paul Gilbert", "dreammaster", ""); + add_person("Tor Andersson", "", "GLK library"); + add_person("Stefan Jokisch", "", "Frotz interpreter"); + add_person("Alan Cox", "", "ScottFree interpreter"); + end_section(); begin_section("Gnap"); add_person("Arnaud Boutonné", "Strangerke", ""); |