From a9948c670826e5560ac8d670387b8e41ea6788f8 Mon Sep 17 00:00:00 2001
From: Jeff Squyres <jsquyres@cisco.com>
Date: Wed, 1 Oct 2014 15:08:36 -0700
Subject: [PATCH] github emails: save for posterity

We don't use this script any more (we use gitdub now), but it took a
long time to figure this out.  So I'm putting this script in git just
so that it's in history if we ever need it again.
---
 .../build-server/github-send-commit-mails.pl  | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100755 contrib/dist/build-server/github-send-commit-mails.pl

diff --git a/contrib/dist/build-server/github-send-commit-mails.pl b/contrib/dist/build-server/github-send-commit-mails.pl
new file mode 100755
index 0000000000..35c2a95445
--- /dev/null
+++ b/contrib/dist/build-server/github-send-commit-mails.pl
@@ -0,0 +1,42 @@
+#!/usr/bin/env perl
+
+use strict;
+
+use Cwd;
+
+die "Must specify location of source git repo"
+    if ($#ARGV < 0);
+
+sub doit {
+    my ($cmd, $repo) = @_;
+
+    my $rc;
+    my $outfile = "/tmp/github-send-email-tmp.$$";
+    unlink($outfile);
+    $rc = system("$cmd >$outfile 2>&1");
+    if (0 != $rc) {
+        print "Command failed:
+
+Command: $cmd
+Repo:    $repo
+Output:\n";
+        open(IN, $outfile);
+        print $_
+            while (<IN>);
+        close(IN);
+#        die "Aborting";
+    }
+    unlink($outfile);
+}
+
+foreach my $src_repo (@ARGV) {
+    die "Specified location of source git repo is invalid"
+        if (! -d $src_repo);
+    chdir($src_repo);
+    die "Could not chdir to $src_repo"
+        if (getcwd() != $src_repo);
+
+    doit("/u/mpiteam/git/local/bin/git fetch", $src_repo);
+    doit("/u/mpiteam/git/local/bin/git push email", $src_repo);
+}
+