From 09802e83cd30871c270387064c0151b8859f9027 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 29 Oct 2024 19:46:48 -0700 Subject: [PATCH] chore: mention `#version` in bug report template (#5769) --- .github/ISSUE_TEMPLATE/bug_report.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md index 387453b1428c..a40b86d5fce8 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -39,7 +39,7 @@ Please put an X between the brackets as you perform the following steps: ### Versions -[Output of `#eval Lean.versionString`] +[Output of `#version` or `#eval Lean.versionString`] [OS version, if not using live.lean-lang.org.] ### Additional Information