commit: 412389f71f8a24307e3adba69b38b4b685b04f72

[log]
author: Johan Commelin <johan@commelin.net>

Tue Feb 04 07:10:08 2025 +0100
committer: GitHub <noreply@github.com>

Tue Feb 04 06:10:08 2025 +0000
tree: 582f1b4f5dfa328fa78a264cc7089b5afadbc891
parent: b385949dd4d2374abd708ba2a6960c44003579d0 [diff]

chore: add commit hash to error message in script/release_notes.py (#6944)

This PR adds a commit hash to the message that `script/release_notes.py`
prints when it can not find a PR number.

script/release_notes.py[diff]

1 file changed

tree: 582f1b4f5dfa328fa78a264cc7089b5afadbc891

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).