Skip to content

Commit 3dd45e7

Browse files
authored
Update coq-timing-diff.yml with optional build target
1 parent 3845b15 commit 3dd45e7

File tree

1 file changed

+7
-1
lines changed

1 file changed

+7
-1
lines changed

.github/workflows/coq-timing-diff.yml

+7-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,12 @@ name: CI (Coq, timing-diff, docker, dev)
22

33
on:
44
workflow_dispatch:
5+
inputs:
6+
build_target:
7+
description: 'Build target for timing diff'
8+
required: false
9+
# default: 'standalone-ocaml lite-generated-files'
10+
type: string
511

612
jobs:
713
build:
@@ -97,7 +103,7 @@ jobs:
97103
98104
# Run the timing diff script
99105
eval $(opam env)
100-
etc/coq-scripts/timing/make-pretty-timed-diff-branch.sh "$BASE_SHA" "$CURRENT_BRANCH"
106+
etc/coq-scripts/timing/make-pretty-timed-diff-branch.sh "$BASE_SHA" "$CURRENT_BRANCH" ${{ github.event.inputs.build_target }}
101107
102108
- name: Display commits between base and current
103109
run: |

0 commit comments

Comments
 (0)