diff --git a/doc/project_list.php b/doc/project_list.php
index e83c33c129..60ee721254 100644
--- a/doc/project_list.php
+++ b/doc/project_list.php
@@ -54,9 +54,6 @@ foreach($proj_list as $p) {
         echo "    <platforms>\n";
         foreach ($platforms as $platform) {
             if ($platform == 'Unknown') continue;
-            if (strstr($platform, "arm-android-linux-gnu")) {
-                $platform = "arm-android-linux-gnu";
-            }
             echo "        <name>$platform</name>\n";
         }
         echo "    </platforms>\n";