From edb158f2d345b3621e768dd30320388611bd6f67 Mon Sep 17 00:00:00 2001 From: Henry Date: Thu, 19 May 2016 10:30:28 -0700 Subject: [PATCH] [Website] Added push to website repo --- build-docs.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/build-docs.sh b/build-docs.sh index abdb7bbdbd..9fdfdc91d3 100755 --- a/build-docs.sh +++ b/build-docs.sh @@ -57,3 +57,4 @@ echo "git add ." git add . echo "git commit -m \"Docs updated from build build $BUILD_SHA\"" git commit -m "Docs updated from build build $BUILD_SHA" +git push