aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--scripts/pushdoc.sh6
1 files changed, 3 insertions, 3 deletions
diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh
index ccae6c9..653d599 100644
--- a/scripts/pushdoc.sh
+++ b/scripts/pushdoc.sh
@@ -4,12 +4,12 @@ set -e # exit with nonzero exit code if anything fails
4# Build documentation 4# Build documentation
5cabal haddock 5cabal haddock
6 6
7# Go to haddock output dir
8cd dist/doc/html/hmacaroons
9
10# Copy benchmark 7# Copy benchmark
11cp benchmark.html dist/doc/html/hmacaroons 8cp benchmark.html dist/doc/html/hmacaroons
12 9
10# Go to haddock output dir
11cd dist/doc/html/hmacaroons
12
13# Quiet the git init message, since it's not useful in the build log 13# Quiet the git init message, since it's not useful in the build log
14git init > /dev/null 2>&1 14git init > /dev/null 2>&1
15 15