[ re #80 ] Removing &>/dev/null

This should be reverted at the end: this redirection is here to avoid leaking information about the token when a push fails.
agda · Jul 13, 2017 · b941190 · b941190
1 parent 67186a0
commit b941190
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.travis.yml b/.travis.yml
@@ -52,7 +52,7 @@ after_success:
   - git fetch upstream && git reset upstream/gh-pages
   - git add -f \*.html
   - git commit -m "Automatic HTML update via Travis"
-  - git push -q upstream HEAD:gh-pages &>/dev/null
+  - git push -q upstream HEAD:gh-pages
 
 notifications:
   email: false