From ad77e7e7629bca30bad63eb511720f20e34e418b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Nov 2023 18:40:55 +0100 Subject: [PATCH] chore: Issue template: Suggest `#eval Lean.versionString` (#2884) as this works also on https://live.lean-lang.org/ or for people not familiar with the command line. --- .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 2c704629b2..0e75ac87ec 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -33,7 +33,7 @@ assignees: '' ### Versions -[Output of `lean --version` in the folder that the issue occured in] +[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in] [OS version] ### Additional Information