aboutsummaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorJohn MacFarlane <jgm@berkeley.edu>2021-03-16 13:01:38 -0700
committerJohn MacFarlane <jgm@berkeley.edu>2021-03-16 13:01:38 -0700
commit2770f88d53c1b4699621e39a4fa254c0cd13f19b (patch)
tree184ba4b0188c72f614ce3189001a4cf5251141fa /.github
parentd0af5795f1de5a75028d48b2d48105d435cbbac3 (diff)
downloadpandoc-2770f88d53c1b4699621e39a4fa254c0cd13f19b.tar.gz
Fix benchmark CI to use gauge options.
Diffstat (limited to '.github')
-rw-r--r--.github/workflows/ci.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b9c5225f3..9a8759f4a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -257,4 +257,4 @@ jobs:
cabal $v2-build --enable-optimization=1 --enable-benchmarks --disable-tests 2>&1 | tee build.log
# fail if warnings in local build
! grep -q ": *[Ww]arning:" build.log || exit 1
- cabal $v2-bench --enable-optimization=1 --benchmark-options='--timeout=6 +RTS -T -RTS'
+ cabal $v2-bench --enable-optimization=1 --benchmark-options='--small'