diff --git a/Lake/CLI/Help.lean b/Lake/CLI/Help.lean index 610cb196af..0f42c8fdc3 100644 --- a/Lake/CLI/Help.lean +++ b/Lake/CLI/Help.lean @@ -62,11 +62,11 @@ errors and prints the list of available scripts. You can pass -h/--help after the script name to print its docstring." -def helpServer := +def helpServe := "Start the Lean language server USAGE: - lake server [-- ...] + lake serve [-- ...] Run the language server of the Lean installation (i.e., via `lean --server`) with the package configuration's `moreServerArgs` field and `args`. @@ -131,7 +131,7 @@ def helpCmd : (cmd : String) → String | "new" => helpNew | "init" => helpInit | "run" => helpRun -| "server" => helpServer +| "serve" => helpServe | "configure" => helpConfigure | "build" => helpBuild | "clean" => helpClean diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 2be28176ec..38086ab7b0 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -232,7 +232,7 @@ def printPaths (imports : List String := []) : CliM PUnit := do else exit noConfigFileCode -def server (leanInstall : LeanInstall) (pkg : Package) (args : List String) : CliM PUnit := do +def serve (leanInstall : LeanInstall) (pkg : Package) (args : List String) : CliM PUnit := do let child ← IO.Process.spawn { cmd := leanInstall.lean.toString, args := #["--server"] ++ pkg.moreServerArgs ++ args @@ -246,7 +246,7 @@ def command : (cmd : String) → CliM PUnit | "new" => do noArgsRem <| new (← takeArg) | "init" => do noArgsRem <| init (← takeArg) | "run" => do noArgsRem <| script (← loadPkg []) (← takeArg) (← getSubArgs) -| "server" => do noArgsRem <| server (← getLeanInstall) (← loadPkg []) (← getSubArgs) +| "serve" => do noArgsRem <| serve (← getLeanInstall) (← loadPkg []) (← getSubArgs) | "configure" => do noArgsRem <| configure (← loadPkg (← getSubArgs)) | "print-paths" => do printPaths (← takeArgs) | "build" => do runBuildM (← loadPkg (← getSubArgs)) <| build (← takeArgs)