diff options
| -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 25ef73c341..ec6a22e558 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -628,7 +628,9 @@ begin_credits("Credits"); add_person("Paul Gilbert", "dreammaster", ""); add_person("Tor Andersson", "", "GarGlk library"); add_person("Stefan Jokisch", "", "Frotz interpreter"); + add_person("Andrew Plotkin", "", "Glulxe interpreter"); add_person("Alan Cox", "", "ScottFree interpreter"); + add_person("Michael J. Roberts", "", "TADS interpreter"); end_section(); begin_section("Gnap"); |