By popular demand from Linux-heads(!), renamed developers to developers.txt.
diff --git a/Misc/developers b/Misc/developers.txt
similarity index 100%
rename from Misc/developers
rename to Misc/developers.txt