File tree 1 file changed +5
-2
lines changed
1 file changed +5
-2
lines changed Original file line number Diff line number Diff line change @@ -38,12 +38,15 @@ jobs:
38
38
- name : compute base sha and current branch
39
39
id : git_ids
40
40
run : |
41
+ git remote add upstream https://github.com/mit-plv/fiat-crypto.git
42
+ git remote update
41
43
# Get the current branch name
42
44
CURRENT_BRANCH=${GITHUB_REF#refs/heads/}
45
+ echo "Current branch: $CURRENT_BRANCH"
43
46
44
47
# Check if this is a PR
45
48
# Check if this branch has an associated PR
46
- PR_NUMBER=$(gh pr list --head $CURRENT_BRANCH --json number --jq '.[0].number')
49
+ PR_NUMBER=$(gh pr list --repo mit-plv/fiat-crypto -- head $CURRENT_BRANCH --json number --jq '.[0].number')
47
50
if [[ -n "$PR_NUMBER" ]]; then
48
51
# Get the base branch from the PR
49
52
BASE_BRANCH=$(gh pr view $PR_NUMBER --json baseRefName --jq '.baseRefName')
57
60
fi
58
61
59
62
echo "Using base SHA: $BASE_SHA"
60
- echo "Current branch: $CURRENT_BRANCH"
61
63
git log --oneline $BASE_SHA..$CURRENT_BRANCH
62
64
63
65
echo "base_sha=${BASE_SHA}" >> $GITHUB_OUTPUT
94
96
CURRENT_BRANCH=${{ steps.git_ids.outputs.current_branch }}
95
97
96
98
# Run the timing diff script
99
+ eval $(opam env)
97
100
etc/coq-scripts/timing/make-pretty-timed-diff-branch.sh "$BASE_SHA" "$CURRENT_BRANCH"
98
101
99
102
- name : Display commits between base and current
You can’t perform that action at this time.
0 commit comments