user-manual: more explanation of push and pull usage

diff --git a/Documentation/build-docdep.perl b/Documentation/build-docdep.perl
index 489389c32af57d39bb843e2b0621144b38006fa3..ba4205e0302a267a5da6bef504f3e69eb0c4aa6d 100755 (executable)
--- a/Documentation/build-docdep.perl
+++ b/Documentation/build-docdep.perl
@@ -41,10 +41,6 @@
 while (my ($text, $included) = each %include) {
     if (! exists $included{$text} &&
        (my $base = $text) =~ s/\.txt$//) {
-       my ($suffix) = '1';
-       if ($base eq 'git') {
-           $suffix = '7'; # yuck...
-       }
-       print "$base.html $base.$suffix : ", join(" ", keys %$included), "\n";
+       print "$base.html $base.xml : ", join(" ", keys %$included), "\n";
     }
 }