diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/pushdoc.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh index 34c811a..ccae6c9 100644 --- a/scripts/pushdoc.sh +++ b/scripts/pushdoc.sh | |||
| @@ -7,6 +7,9 @@ cabal haddock | |||
| 7 | # Go to haddock output dir | 7 | # Go to haddock output dir |
| 8 | cd dist/doc/html/hmacaroons | 8 | cd dist/doc/html/hmacaroons |
| 9 | 9 | ||
| 10 | # Copy benchmark | ||
| 11 | cp benchmark.html dist/doc/html/hmacaroons | ||
| 12 | |||
| 10 | # 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 |
| 11 | git init > /dev/null 2>&1 | 14 | git init > /dev/null 2>&1 |
| 12 | 15 | ||