diff options
-rw-r--r-- | scripts/pushdoc.sh | 6 |
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 |
5 | cabal haddock | 5 | cabal haddock |
6 | 6 | ||
7 | # Go to haddock output dir | ||
8 | cd dist/doc/html/hmacaroons | ||
9 | |||
10 | # Copy benchmark | 7 | # Copy benchmark |
11 | cp benchmark.html dist/doc/html/hmacaroons | 8 | cp benchmark.html dist/doc/html/hmacaroons |
12 | 9 | ||
10 | # Go to haddock output dir | ||
11 | cd 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 |
14 | git init > /dev/null 2>&1 | 14 | git init > /dev/null 2>&1 |
15 | 15 | ||