max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: improve bug report template instructions (#11537)

Browse source 
This PR makes it so that in the issue template a line about how to check
boxes is in comment form you can only see it when you are creating the
issue and it does not need to be displayed to everyone.
This commit is contained in:
Gabe 2025-12-07 13:52:52 -06:00 • committed by GitHub
parent 2ca3bc2859
commit b7ac6243a9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/ISSUE_TEMPLATE/bug_report.md vendored
View file

@ -9,7 +9,7 @@ assignees: ''
### Prerequisites
Please put an X between the brackets as you perform the following steps:
<!-- Please put an X between the brackets as you perform the following steps: -->
* [ ] Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues