From 7b64a6cc9447f87e205d9b9d41ad5b88f632c31a Mon Sep 17 00:00:00 2001 From: ia0 Date: Tue, 11 Aug 2026 15:36:00 +0200 Subject: [PATCH] doc: fix default format for lake init --- Manual/BuildTools/Lake/CLI.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index 3b3ae32b1..29a5821be 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -458,7 +458,7 @@ The {lakeMeta}`template` may be: Creates a package that contains a library that depends on [Mathlib](https://github.com/leanprover-community/mathlib4). -The {lakeMeta}`language` selects the file format used for the {tech}[package configuration] file and may be `lean` (the default) or `toml`. +The {lakeMeta}`language` selects the file format used for the {tech}[package configuration] file and may be `lean` or `toml` (the default). ::: :::TODO