Skip to content

Commit bcf63b0

Browse files
fix: missing text
1 parent 7a3ae72 commit bcf63b0

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

Manual/BuildTools/Lake.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -405,6 +405,10 @@ The facets available for modules are:
405405

406406
The parsed module header of the module's source file.
407407

408+
: `input`
409+
410+
The module's processed Lean source file. Combines tracing the file with parsing its header.
411+
408412
: `imports`
409413

410414
The immediate imports of the Lean module, but not the full set of transitive imports.
@@ -458,10 +462,6 @@ The facets available for modules are:
458462

459463
A shared library (e.g., for the Lean option `--load-dynlib`){TODO}[Document Lean command line options, and cross-reference from here].
460464

461-
: `input`
462-
463-
TODO
464-
465465
:::
466466

467467

0 commit comments

Comments
 (0)