chore: Try to fix docs
This commit is contained in:
parent
116aa11660
commit
9a33bb899a
2 changed files with 1 additions and 1 deletions
|
@ -66,6 +66,7 @@ srcDir = "scripts/MetaPrograms"
|
|||
|
||||
[[lean_exe]]
|
||||
name = "informal"
|
||||
supportInterpreter = true
|
||||
srcDir = "scripts/MetaPrograms"
|
||||
|
||||
# -- Optional inclusion of openAI_doc_check. Needs `llm` above.
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue