From 293c19d24ffad3a403a1689d6bcec48e0c472701 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 31 Jul 2021 19:29:26 -0400 Subject: [PATCH] feat: include Lean version in Lake usage header --- Lake/Help.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Lake/Help.lean b/Lake/Help.lean index faeefe2604..452d72345e 100644 --- a/Lake/Help.lean +++ b/Lake/Help.lean @@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ import Lake.Version +import Lake.LeanVersion namespace Lake def usage := -"Lake, version " ++ versionString ++ " +s!"Lake version {versionString} (Lean version {uiLeanVersionString}) Usage: lake