travis: Be less verbose when pushing.
This commit is contained in:
parent
069f80789d
commit
d690fd616d
|
|
@ -1,7 +1,6 @@
|
||||||
#! /bin/bash
|
#! /bin/bash
|
||||||
|
|
||||||
set -e
|
set -e
|
||||||
set -x
|
|
||||||
|
|
||||||
if [ ! -d html ]; then
|
if [ ! -d html ]; then
|
||||||
echo "Please generate the html files first."
|
echo "Please generate the html files first."
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue