lean4-htt/.github
Scott Morrison 1f68dec119
chore: fix commit used for PR release (#2861)
We were checking out the synthetic merge commit between the PR `HEAD`
and `master`, and this was then breaking the logic to determine which
nightly-testing branches to use in Mathlib and Std.
2023-11-11 00:35:27 +00:00
..
ISSUE_TEMPLATE chore: remove 'reproduces how often' field from bug template 2023-09-15 14:24:21 +02:00
workflows chore: fix commit used for PR release (#2861) 2023-11-11 00:35:27 +00:00
PULL_REQUEST_TEMPLATE.md doc: Update contribution guides (#2624) 2023-10-25 13:05:55 +11:00