use git-fetch --prune

otherwise dead mainlines accumulate, as for example when we changed
branching schemes.

Change-Id: Ia5bcb90a079dc62c3c848d139cef5f6d6e0ccbba
Reviewed-by: Orgad Shaneh <orgads@gmail.com>

git-hooks/gerrit-bot

@@ -128,7 +128,7 @@ sub process_commit($$$$$)
         chomp(@mainlines = `git config remote.origin.fetch`);
         $skipfetch{$project} = 1;
       }
-      if (system("git", "fetch", "-f", "origin", $ref.":refs/changes/".$number, @mainlines)) {
+      if (system("git", "fetch", "-f", "--prune", "origin", $ref.":refs/changes/".$number, @mainlines)) {
         printerr "GIT fetch of ".$ref." from ".$project." failed";
         return;
       }