aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rwxr-xr-xpage6
1 files changed, 6 insertions, 0 deletions
diff --git a/page b/page
index 94d9586297..7b375f2b59 100755
--- a/page
+++ b/page
@@ -5,6 +5,9 @@ use File::Spec;
-d '.git' or die "$0: Not a Git repository";
+my $no_push = 0;
+$no_push = @ARGV && $ARGV[0] eq '-n';
+
my $root = dirname($0);
my $application = "$root/application";
my $last = `(cd $root; git ls-files "whats" | tail -1)`;
@@ -92,3 +95,6 @@ print "</html>\n";
close STDOUT;
system qq(cd GH-PAGES; git commit --amend -m "Update index.html" index.html >/dev/null);
+
+system qq(cd GH-PAGES; git push erlang +gh-pages)
+ unless $no_push;